		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 for which the generated theorem (if any) has hypotheses about the variables being in the computation state and having values of the appropriate types.

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.
Simpadd0-gout-equiv: Basic equivalence relation for simpadd0-gout structures.
Make-simpadd0-gout: Basic constructor macro 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.
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.
Change-simpadd0-gout: Modifying constructor for simpadd0-gout structures.