		Search-engine friendly clone of the ACL2 documentation.

Atc-gen-expr-pure

Generate a C expression from an ACL2 term that must be a pure expression term.

Signature
(atc-gen-expr-pure term gin state) → (mv erp gout)
Arguments: term — Guard (pseudo-termp term).; gin — Guard (expr-ginp gin).
Returns: gout — Type (expr-goutp gout).

At the same time, we check that the term is a pure expression term, as described in the user documentation. Based on its form, we dispatch to different code, after recursively processing sub-expressions.