Search-engine friendly clone of the
ACL2 documentation
.
Top
Pass-result
Pass-result-ok
This is a product type, introduced by
fty::defflexsum
in support of
pass-result
.
Fields
get —
pass
Subtopics
Pass-result-ok->get
Get the
get
field from a
pass-result-ok
.
Make-pass-result-ok
Basic constructor macro for
pass-result-ok
structures.
Change-pass-result-ok
Modifying constructor for
pass-result-ok
structures.