		Search-engine friendly clone of the ACL2 documentation.

Expr-gout

Outputs for C pure expression generation.

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

expr — expr: Expression generated from the term.
type — type: The type returned by the expression. Never void.
term — pseudo-term: The term from which the expression is generated. The term is transformed by replacing if with if*.
events — pseudo-event-form-list: All the events generated for the expression.
thm-name — symbolp: The name of the theorem about exec-expr-pure applied to the expression. This theorem is one of the events in events. It is nil if no theorem was generated, which happens exactly when the proofs flag in expr-gin is nil.
thm-index — posp: Described in atc-implementation.
names-to-avoid — symbol-list: Described in atc-implementation.