Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Apt
Zfc
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
C
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
Java
Riscv
Taspi
Bitcoin
Des
Ethereum
X86isa
Sha-2
Yul
Zcash
Proof-checker-itp13
Regex
ACL2-programming-language
Json
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Axe
Aleo
Aleobft
Aleovm
Leo
Grammar
Early-version
Json2ast
Testing
Definition
Flattening
Abstract-syntax
Dynamic-semantics
Execution
Exec-expressions/statements
Init-for-loop
Exec-file-main
Update-variable-value-in-scope-list
Step-for-loop
Update-variable-value-in-scope
Expr-value-to-value
Exec-binary
Exec-expression
Init-vcscope-dinfo-call
Value?+denv
Exec-statement
End-of-for-loop-p
Expr-value
Evalue+denv
Write-location
Read-location
Exec-for-loop-iterations
Update-variable-value
Exec-unary
Values+denv
Init-vcscope-dinfo-loop
Extend-denv-with-structdecl
Exec-var/const
Valuemap+denv
Namevalue+denv
Extend-denv-with-fundecl
Ensure-boolean
Int+denv
Push-vcscope-dinfo
Extend-denv-with-topdecl-list
Exec-literal
Build-denv-from-file
Namevalue+denv-result
Extend-denv-with-topdecl
Evalue+denv-result
Evalue+denv-result-fix
Evalue+denv-result-equiv
Evalue+denv-resultp
Evalue+denv-result-ok
Evalue+denv-result-err
Evalue+denv-result-err->get
Make-evalue+denv-result-err
Change-evalue+denv-result-err
Evalue+denv-result-kind
Value?+denv-result
Values+denv-result
Valuemap+denv-result
Int+denv-result
Push-call-dinfo
Exec-print
Pop-vcscope-dinfo
Exec-if
Exec-function
Pop-call-dinfo
Exec-statement-list
Exec-block
Exec-struct-init-list
Exec-struct-init
Exec-expression-list
Values
Dynamic-environments
Arithmetic-operations
Curve-parameterization
Shift-operations
Errors
Value-expressions
Locations
Input-execution
Edwards-bls12-generator
Equality-operations
Logical-operations
Program-execution
Ordering-operations
Bitwise-operations
Literal-evaluation
Type-maps-for-struct-components
Output-execution
Tuple-operations
Struct-operations
Compilation
Static-semantics
Concrete-syntax
Bigmems
Builtins
Execloader
Solidity
Paco
Concurrent-programs
Bls12-377-curves
Debugging
Community
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Evalue+denv-result
Evalue+denv-result-err
This is a product type, introduced by
fty::defflexsum
in support of
evalue+denv-result
.
Fields
get —
reserr
Subtopics
Evalue+denv-result-err->get
Get the
get
field from a
evalue+denv-result-err
.
Make-evalue+denv-result-err
Basic constructor macro for
evalue+denv-result-err
structures.
Change-evalue+denv-result-err
Modifying constructor for
evalue+denv-result-err
structures.