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