Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Def-error-checker
Def-error-checker-implementation
Def-error-checker-fn
Def-error-checker-bindings
Def-error-checker-x-symbols
Def-error-checker-macro-definition
Def-error-checker-table
Ensure-function/macro/lambda
Ensure-symbol-is-fresh-event-name
Ensure-function/lambda/term-number-of-results
Ensure-function/lambda-arity
Ensure-function/lambda-no-stobjs
Ensure-function/lambda-guard-verified-fns
Ensure-function-name-or-numbered-wildcard
Ensure-function/lambda-logic-mode
Ensure-function/lambda-closed
Ensure-value-is-untranslated-term
Ensure-function-number-of-results
Ensure-boolean-or-auto-and-return-boolean
Ensure-is-hints-specifier
Ensure-term-if-call
Ensure-value-is-not-in-list
Ensure-term-free-vars-subset
Ensure-symbol-new-event-name
Ensure-symbol-different
Ensure-function/lambda-guard-verified-exec-fns
Ensure-value-is-in-list
Ensure-list-subset
Ensure-function-no-stobjs
Ensure-function-known-measure
Ensure-term-not-call-of
Ensure-lambda-guard-verified-fns
Ensure-term-guard-verified-fns
Ensure-term-does-not-call
Ensure-lambda-logic-mode
Ensure-lambda-arity
Ensure-function-singly-recursive
Ensure-function-is-pure-if-raw
Ensure-function-arity
Ensure-term-no-stobjs
Ensure-term-logic-mode
Ensure-list-functions
Ensure-keyword-value-list
Ensure-function-program-mode
Ensure-function-non-recursive
Ensure-function-is-logic-mode
Ensure-function-is-guard-verified
Ensure-function-is-defined
Ensure-value-is-legal-variable-name
Ensure-value-is-function-name
Ensure-value-is-constant-name
Ensure-term-ground
Ensure-symbol-truelist-alist
Ensure-symbol-not-stobj
Ensure-symbol-function
Ensure-list-has-no-duplicates
Ensure-lambda-closed
Ensure-function-recursive
Ensure-function-name-list
Ensure-function-has-args
Ensure-value-is-true-list
Ensure-value-is-symbol-list
Ensure-tuple
Ensure-symbol-not-keyword
Ensure-defun-mode-or-auto
Ensure-value-is-symbol
Ensure-value-is-string
Ensure-value-is-boolean
Ensure-symbol-alist
Ensure-string-or-nil
Ensure-doublet-list
Ensure-defun-mode
Ensure-constant-name
Ensure-boolean-or-auto
Ensure-value-is-nil
Ensure-function-not-in-termination-thm
Ensure-lambda-guard-verified-exec-fns
Ensure-term-guard-verified-exec-fns
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Def-error-checker
Def-error-checker-implementation
Implementation of
def-error-checker
.
Subtopics
Def-error-checker-fn
Generate the function and the macro.
Def-error-checker-bindings
Generate the
b*
bindings of the error checking function.
Def-error-checker-x-symbols
Turn each
xi
symbol into itself and each
xi
extended formal into its underlying symbol.
Def-error-checker-macro-definition
Definition of the
def-error-checker
macro.
Def-error-checker-table
Table of successful
def-error-checker
calls.