		Search-engine friendly clone of the ACL2 documentation.

Const-expr

Fixtype of constant expressions [C:6.6] [C:A.2.1].

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

Fields

expr — expr

This corresponds to constant-expression in the grammar in [C]. As in that grammar, it does not actually constrain the expression to be constant, but it may be useful to mark expressions to be constant, with separate predicates that enforce that.

Subtopics

Const-expr-equiv: Basic equivalence relation for const-expr structures.
Const-exprp: Recognizer for const-expr structures.
Make-const-expr: Basic constructor macro for const-expr structures.
Const-expr->expr: Get the expr field from a const-expr.
Change-const-expr: Modifying constructor for const-expr structures.
Const-expr-fix: Fixing function for const-expr structures.
Const-expr-count: Measure for recurring over const-expr structures.