		Search-engine friendly clone of the ACL2 documentation.

Exprs-gin

Inputs for C pure expression list generation.

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

context — atc-context: Described in atc-implementation. It is the context just before these expressions, i.e. the context in which these expressions are generated.
inscope — atc-symbol-varinfo-alist-list: Described in atc-implementation. It contains the variables in scope just before these expressions, i.e. the ones in scope for these expressions.
prec-tags — atc-string-taginfo-alist: Described in atc-implementation.
fn — symbolp: Described in atc-implementation. It is the target function for which the expressions are generated.
fn-guard — symbolp: Described in atc-implementation.
compst-var — symbolp: Described in atc-implementation.
thm-index — posp: Described in atc-implementation.
names-to-avoid — symbol-list: Described in atc-implementation.
proofs — booleanp: A flag indicating whether modular proof generation should continue or not. This will be eliminated when modular proof generation will cover all of the ATC-generated code.

This does not include the terms, which are passed as a separate input.