		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gin

General inputs for transformation functions.

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

Fields

const-new — symbolp: The :const-new input of the transformation.
thm-index — posp: Index used to generate unique theorem names that include increasing numeric indices.
names-to-avoid — symbol-list: List of event names to avoid, for the generated theorems.

The transformation functions take as input the construct to transform, which has a different type for each transformation function. But each function also takes certain common inputs, which we put into this data structure for modularity and to facilitate extension. Additionally, the transformation take the ACL2 state as input, but this is not part of this structure for obvious reasons.

Subtopics

Simpadd0-ginp: Recognizer for simpadd0-gin structures.
Simpadd0-gin-fix: Fixing function for simpadd0-gin structures.
Simpadd0-gin-equiv: Basic equivalence relation for simpadd0-gin structures.
Make-simpadd0-gin: Basic constructor macro for simpadd0-gin structures.
Simpadd0-gin->names-to-avoid: Get the names-to-avoid field from a simpadd0-gin.
Simpadd0-gin->thm-index: Get the thm-index field from a simpadd0-gin.
Simpadd0-gin->const-new: Get the const-new field from a simpadd0-gin.
Change-simpadd0-gin: Modifying constructor for simpadd0-gin structures.