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
Gl
Esim
Vl2014
Sv
Vwsim
Fgl
Fgl-rewrite-rules
Fgl-function-mode
Fgl-object
Fgl-solving
Fgl-handling-if-then-elses
Fgl-getting-bits-from-objects
Fgl-primitive-and-meta-rules
Fgl-interpreter-overview
Fgl-counterexamples
Fgl-correctness-of-binding-free-variables
Fgl-debugging
Fgl-testbenches
Def-fgl-boolean-constraint
Fgl-stack
Scratchobj
Scratchobj-fix
Scratchobj-case
Scratchobj-equiv
Scratchobj-p
Scratchobj-fgl-objlist
Scratchobj-fgl-obj
Scratchobj-cinstlist
Scratchobj-cinst
Scratchobj-cinst->val
Make-scratchobj-cinst
Change-scratchobj-cinst
Scratchobj-bfrlist
Scratchobj-bfr
Scratchobj-kind
Minor-frame
Major-frame
Major-stack
Scratchlist
Minor-stack
Fgl-rewrite-tracing
Def-fgl-param-thm
Def-fgl-thm
Fgl-fast-alist-support
Fgl-array-support
Advanced-equivalence-checking-with-fgl
Fgl-internals
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Scratchobj
Scratchobj-cinst
This is a product type, introduced by
fty::deftagsum
in support of
scratchobj
.
Fields
val —
constraint-instance
Subtopics
Scratchobj-cinst->val
Get the
val
field from a
scratchobj-cinst
.
Make-scratchobj-cinst
Basic constructor macro for
scratchobj-cinst
structures.
Change-scratchobj-cinst
Modifying constructor for
scratchobj-cinst
structures.