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
Abstract-syntax
Expression
Expressionp
Expression-case
Expression-sum-field
Expression-sum-update
Expression-equiv
Expression-kind
Expression-product-field
Expression-when
Expression-unless
Expression-sum-test
Expression-sum-construct
Expression-product-update
Expression-if
Expression-call
Expression-bind
Expression-binary
Expression-product-construct
Expression-unary
Expression-component
Expression-variable
Expression-variable->name
Make-expression-variable
Change-expression-variable
Expression-multi
Expression-literal
Expression-cond
Expression-bad-expression
Expression-fix
Expression-count
Expression-sum-field-list
Type
Binary-op
Expression-product-field-list
Abstract-syntax-operations
Function-definition-list->header-list
Type-definition-list->name-list
Initializer-list->value-list
Function-header-list->name-list
Typed-variable-list->type-list
Typed-variable-list->name-list
Branch-list->condition-list
Alternative-list->name-list
Function-specifier
Expression-variable-list
Type-subset
Field-list->type-list
Field-list->name-list
Function-specification
Identifier
Toplevel
Function-definer
Function-header
Type-definer
Literal
Type-product
Function-definition
Type-sum
Maybe-expression
Transform-argument-value
Transform
Theorem
Quantifier
Maybe-function-specification
Maybe-typed-variable
Maybe-type-definition
Maybe-function-header
Maybe-function-definition
Maybe-type-sum
Maybe-type-subset
Maybe-type-product
Maybe-type-definer
Maybe-theorem
Maybe-type
Initializer
Type-definition
Alternative
Unary-op
Typed-variable
Branch
Field
Transform-argument
Type-recursion
Program
Function-recursion
Typed-variable-list
Toplevel-name
Toplevel-list
Initializer-list
Expression-fixtypes
Toplevel-fn-names
Lookup-transform-argument
Function-definition-names
Type-definition-list
Transform-argument-list
Function-header-list
Function-definition-list
Alternative-list
Type-list
Identifier-set
Identifier-list
Field-list
Expression-list
Branch-list
Extract-default-param-alist
Create-arg-defaults-table
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
Expression
Expression-variable
This is a product type, introduced by
fty::deftagsum
in support of
expression
.
Fields
name —
identifier
Subtopics
Expression-variable->name
Get the
name
field from a
expression-variable
.
Make-expression-variable
Basic constructor macro for
expression-variable
structures.
Change-expression-variable
Modifying constructor for
expression-variable
structures.