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
Outcome
Abstract-syntax-operations
Subst-expression-fns
Subst-expression
Subst-initializer-list
Subst-initializer
Subst-expression-list
Subst-branch-list
Subst-branch
Field-list-to-typed-variable-list
Negate-expression
Get-function-definition-in-function-definitions
Get-function-definition
Get-type-definition-in-type-definitions
Get-type-definition
Get-function-specification
Get-type-subset
Get-alternative-product
Direct-supertype
Get-function-header-in-list
Equate-expression-lists
Get-field-type
Get-theorem
Get-defined-type-names-in-type-definitions
Disjoin-expressions
Conjoin-expressions
Get-type-product
Binary-op-nonstrictp
Get-type-sum
Get-defined-type-names
Equate-expressions
Field-to-typed-variable
Subst-expression
Binary-op-strictp
Initializer-list-from-flds-vals
Typed-variable-list->-expression-variable-list
Typed-variable-list->-expression
Variable-substitution
Local-variables
Identifier-list-names
Functions-called
Subst-expression-list
Subst-branch-list
Subst-branch
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
Subst-expression-fns
Subst-initializer
Apply a substitution to an initializer.
Signature
(subst-initializer subst init) → new-init
Arguments
subst
—
Guard
(
variable-substitutionp
subst)
.
init
—
Guard
(
initializerp
init)
.
Returns
new-init
—
Type
(
initializerp
new-init)
.