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