		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gout

General outputs for transformation functions.

This is a product type introduced by fty::defprod.

Fields

events — pseudo-event-form-list: Cumulative list of generated theorems.
thm-name — symbolp: Name of the theorem generated by the transformation function. The theorem concerns the transformation of the C construct that the transformation function operates on. This is nil if no theorem is generated.
thm-index — posp: Updated numeric index to generate unique theorem names; this is updated from the homonymous component of simpadd0-gin.
names-to-avoid — symbol-list: Updated list of event names to avoid; this is updated from the homonymous component of simpadd0-gin.
vartys — ident-type-map: Variables in scope, with their types.
diffp — booleanp: Flag saying whether the C construct was transformed into something different by the transformation function.

The transformation functions return as output the transformed construct, which has a different type for each transformation function. But each function also returns certain common outputs, which we put into this data structure for modularity and to facility extension.

Subtopics

Simpadd0-goutp: Recognizer for simpadd0-gout structures.
Simpadd0-gout-fix: Fixing function for simpadd0-gout structures.
Make-simpadd0-gout: Basic constructor macro for simpadd0-gout structures.
Simpadd0-gout-equiv: Basic equivalence relation for simpadd0-gout structures.
Simpadd0-gout->names-to-avoid: Get the names-to-avoid field from a simpadd0-gout.
Simpadd0-gout->events: Get the events field from a simpadd0-gout.
Change-simpadd0-gout: Modifying constructor for simpadd0-gout structures.
Simpadd0-gout->vartys: Get the vartys field from a simpadd0-gout.
Simpadd0-gout->thm-name: Get the thm-name field from a simpadd0-gout.
Simpadd0-gout->thm-index: Get the thm-index field from a simpadd0-gout.
Simpadd0-gout->diffp: Get the diffp field from a simpadd0-gout.