		Search-engine friendly clone of the ACL2 documentation.

Valid-const-expr

Validate a constant expression.

Signature
(valid-const-expr cexpr table ienv) → (mv erp new-cexpr type return-types new-table)
Arguments: cexpr — Guard (const-exprp cexpr).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-cexpr — Type (const-exprp new-cexpr).; type — Type (typep type).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

Besides being valid expressions, constant expression must satisfy other requirements [C17:6.6]. Fow now we do not check these requirements, but when we do we may need to extend this validation function to return not only a type but also a value, namely the value of the constant expression.