Search-engine friendly clone of the
ACL2 documentation
.
Top
Expression
Expression-tuple-component
This is a product type, introduced by
fty::deftagsum
in support of
expression
.
Fields
tuple —
expression
index —
natp
Subtopics
Expression-tuple-component->tuple
Get the
tuple
field from a
expression-tuple-component
.
Expression-tuple-component->index
Get the
index
field from a
expression-tuple-component
.
Make-expression-tuple-component
Basic constructor macro for
expression-tuple-component
structures.
Change-expression-tuple-component
Modifying constructor for
expression-tuple-component
structures.