		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-implementation

Simpadd0-event-generation

Event generation performed by simpadd0.

Subtopics

Simpadd0-exprs/decls/stmts: Transform expressions, declarations, statements, and related entities.
Simpadd0-expr-binary: Transform a binary expression.
Simpadd0-gen-from-params: Generate certain pieces of information from the formal parameters of a function.
Simpadd0-gen-expr-pure-thm: Generate a theorem for the transformation of a pure expression.
Simpadd0-fundef: Transform a function definition.
Simpadd0-gen-block-item-list-thm: Generate a theorem for the transformation of a list of block items.
Simpadd0-gen-block-item-thm: Generate a theorem for the transformation of a block item.
Simpadd0-gen-stmt-thm: Generate a theorem for the transformation of a statement.
Simpadd0-expr-unary: Transform a unary expression.
Simpadd0-gout: General outputs for transformation functions.
Simpadd0-expr-ident: Transform an identifier expression (i.e. a variable).
Simpadd0-expr-const: Transform a constant.
Simpadd0-gen-param-thms: Generate theorems about the parameters of a function.
Simpadd0-block-item-stmt: Transform a block item that consists of a statement.
Simpadd0-block-item-list-one: Transform a singleton list of block items.
Simpadd0-stmt-return: Transform a return statement.
Simpadd0-gen-init-scope-thm: Generate a theorem about the initial scope of a function.
Simpadd0-gin: General inputs for transformation functions.
Simpadd0-expr-paren: Transform a parenthesized expression.
Simpadd0-filepath-transunit-map: Transform a map from file paths to translation units.
Simpadd0-extdecl-list: Transform a list of external declarations.
Simpadd0-extdecl: Transform an external declaration.
Simpadd0-transunit-ensemble: Transform a translation unit ensemble.
Simpadd0-tyspecseq-to-type-and-value-kind: Map a type specifier sequence from the language formalization to the corresponding type and kind of value.
Simpadd0-gen-var-hyps: Generate variable hypotheses for certain theorems.
Simpadd0-transunit: Transform a translation unit.
Simpadd0-gin-update: Update a simpadd0-gin with a simpadd0-gout.
Simpadd0-gen-everything: Event expansion of the transformation.
Irr-simpadd0-gout: Irrelevant general outputs for transformation functions.