		Search-engine friendly clone of the ACL2 documentation.

Pexprs-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.

Pexprs-gin-fix: Fixing function for pexprs-gin structures.
Make-pexprs-gin: Basic constructor macro for pexprs-gin structures.
Pexprs-gin-equiv: Basic equivalence relation for pexprs-gin structures.
Pexprs-ginp: Recognizer for pexprs-gin structures.
Pexprs-gin->prec-tags: Get the prec-tags field from a pexprs-gin.
Pexprs-gin->names-to-avoid: Get the names-to-avoid field from a pexprs-gin.
Pexprs-gin->inscope: Get the inscope field from a pexprs-gin.
Change-pexprs-gin: Modifying constructor for pexprs-gin structures.
Pexprs-gin->compst-var: Get the compst-var field from a pexprs-gin.
Pexprs-gin->thm-index: Get the thm-index field from a pexprs-gin.
Pexprs-gin->proofs: Get the proofs field from a pexprs-gin.
Pexprs-gin->fn-guard: Get the fn-guard field from a pexprs-gin.
Pexprs-gin->context: Get the context field from a pexprs-gin.
Pexprs-gin->fn: Get the fn field from a pexprs-gin.