Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Parallelism
History
Programming
Defun
Declare
System-utilities
Stobj
State
Mutual-recursion
Memoize
Mbe
Io
Defpkg
Apply$
Loop$
Programming-with-state
Arrays
Characters
Time$
Defconst
Loop$-primer
Fast-alists
Defmacro
Evaluation
Guard
Equality-variants
Compilation
Hons
ACL2-built-ins
Developers-guide
System-attachments
Advanced-features
Set-check-invariant-risk
Numbers
Irrelevant-formals
Efficiency
Introduction-to-programming-in-ACL2-for-those-who-know-lisp
Redefining-programs
Lists
Invariant-risk
Errors
Er
Value-triple
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
Error-triple
Assert-event
Set-warnings-as-errors
Hard-error
Set-inhibit-er
Must-fail
Breaks
Assert!-stobj
Must-eval-to
Ctx
Assert!
Must-succeed
Assert$
Illegal
Ctxp
Er-progn
Error1
Er-hard
Must-succeed*
Toggle-inhibit-er
Break$
Assert*
Assert?
Er-soft+
Er-hard?
Must-fail-with-soft-error
Must-fail-with-hard-error
Must-fail-with-error
Must-eval-to-t
Er-soft-logic
Er-soft
Convert-soft-error
Toggle-inhibit-er!
Set-inhibit-er!
Must-prove
Must-not-prove
Must-fail!
Must-be-redundant
Must-succeed!
Must-fail-local
Assert-equal
Defabbrev
Conses
Alists
Set-register-invariant-risk
Strings
Program-wrapper
Get-internal-time
Basics
Packages
Oracle-eval
Defmacro-untouchable
Primitive
<<
Revert-world
Set-duplicate-keys-action
Unmemoize
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Fake-oracle-eval
Defopen
Sleep
Real
Start-here
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
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.