		Search-engine friendly clone of the ACL2 documentation.

Lstmt-gin

Inputs for C loop statement generation.

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

This does not include the term, which is passed as a separate input.

The measure-for-fn component is the name of the locally generated measure function for the target function fn that represents the loop.

Lstmt-gin-fix: Fixing function for lstmt-gin structures.
Make-lstmt-gin: Basic constructor macro for lstmt-gin structures.
Lstmt-ginp: Recognizer for lstmt-gin structures.
Lstmt-gin-equiv: Basic equivalence relation for lstmt-gin structures.
Change-lstmt-gin: Modifying constructor for lstmt-gin structures.
Lstmt-gin->typed-formals: Get the typed-formals field from a lstmt-gin.
Lstmt-gin->prec-tags: Get the prec-tags field from a lstmt-gin.
Lstmt-gin->prec-objs: Get the prec-objs field from a lstmt-gin.
Lstmt-gin->names-to-avoid: Get the names-to-avoid field from a lstmt-gin.
Lstmt-gin->measure-formals: Get the measure-formals field from a lstmt-gin.
Lstmt-gin->measure-for-fn: Get the measure-for-fn field from a lstmt-gin.
Lstmt-gin->prec-fns: Get the prec-fns field from a lstmt-gin.
Lstmt-gin->inscope: Get the inscope field from a lstmt-gin.
Lstmt-gin->compst-var: Get the compst-var field from a lstmt-gin.
Lstmt-gin->thm-index: Get the thm-index field from a lstmt-gin.
Lstmt-gin->proofs: Get the proofs field from a lstmt-gin.
Lstmt-gin->limit-var: Get the limit-var field from a lstmt-gin.
Lstmt-gin->fn-guard: Get the fn-guard field from a lstmt-gin.
Lstmt-gin->fenv-var: Get the fenv-var field from a lstmt-gin.
Lstmt-gin->context: Get the context field from a lstmt-gin.
Lstmt-gin->fn: Get the fn field from a lstmt-gin.