Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
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
Process-syntheto-toplevel-fn
Translation
Language
Static-semantics
Check-expression-fns
Subtypep
Match-type
Check-product-update-expression
Get-builtin-function-in/out/pre-post
Check-sum-update-expression
Check-sum-field-expression
Check-strict-binary-expression
Check-lt/le/gt/ge-expression
Check-eq/ne-expression
Check-div/rem-expression
Check-add/sub/mul-expression
Align-let-vars-values
Check-iff-expression
Check-function-definition-top/nontop
Check-sum-construct-expression
Check-rem-expression
Check-mul-expression
Check-sub-expression
Check-div-expression
Check-add-expression
Check-ne-expression
Check-lt-expression
Check-le-expression
Check-gt-expression
Check-ge-expression
Check-eq-expression
Check-function-specifier
Type-result
Check-product-construct-expression
Supremum-type
Check-call-expression
Check-product-field-expression
Check-function-definer
Make-subproof-obligations
Get-function-in/out/pre/post
Check-sum-test-expression
Match-field
Decompose-expression
Match-to-target
Check-unary-expression
Max-supertype
Match-type-list
Check-minus-expression
Check-type-definition
Check-not-expression
Check-type-product
Match-field-list
Check-type-subset
Check-type-definition-in-recursion
Align-let-vars-values-aux
Non-trivial-proof-obligation
Check-type-recursion
Check-function-specification
Check-toplevel
Supremum-type-list
Check-component-expression
Check-branch-list
Check-function-recursion
Check-function-definition
Binding
Check-function-header
Check-function-definition-list
Check-type-definition-list-in-recursion
Check-theorem
Check-nonstrict-binary-expression
Context-add-variables
Decompose-expression-aux
Check-alternative
Check-multi-expression
Check-type-sum
Check-type
Check-alternative-list
Context-add-condition
Check-type-definer
Check-transform
Check-variable
Check-transform-args
Check-toplevel-list
Context-add-condition-list
Check-if/when/unless-expression
Initializers-to-variable-substitution
Context-add-binding
Check-function-header-list
Context-add-toplevel
Ensure-single-type
Max-supertypes
Check-bind-expression
Check-type-list
Check-literal
Literal-type
Check-expression-list
Variable-context
Check-cond-expression
Check-branch
Args-without-defaults
Check-expression
*builtin-function-names*
Function-called-in
Abstract-syntax
Outcome
Abstract-syntax-operations
Outcome-list
Outcomes
Process-syntheto-toplevel
Shallow-embedding
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Static-semantics
Check-expression-fns
Check-expression
Check if an expression is statically well-formed.
Signature
(check-expression expr ctxt) → result
Arguments
expr
—
Guard
(
expressionp
expr)
.
ctxt
—
Guard
(
contextp
ctxt)
.
Returns
result
—
Type
(
type-resultp
result)
.