Search-engine friendly clone of the
ACL2 documentation
.
Top
Topdecl
Topdecl-mapping
This is a product type, introduced by
fty::deftagsum
in support of
topdecl
.
Fields
get —
mappingdecl
Subtopics
Topdecl-mapping->get
Get the
get
field from a
topdecl-mapping
.
Make-topdecl-mapping
Basic constructor macro for
topdecl-mapping
structures.
Change-topdecl-mapping
Modifying constructor for
topdecl-mapping
structures.