		Search-engine friendly clone of the ACL2 documentation.

Decimal-integer-literals

Dec-integer-literal

Fixtype of decimal integer literals.

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

Fields

digits/uscores — decdig/uscore-list
suffix? — optional-integer-type-suffix

Additional Requirements

The following invariant is enforced on the fields:

(decdig/uscore-list-wfp digits/uscores)

A decimal integer literal consists of (i) a sequence of decimal digits and underscores satisfying the constraints in decdig/uscore-list-wfp, and (ii) an optional integer type suffix.

The set of values of this fixtype should be isomorphic to the set of strings (or parse trees) defined by the Java grammar rule decimal-integer-literal. This remains to be proved formally.

Subtopics

Dec-integer-literal-fix: Fixing function for dec-integer-literal structures.
Dec-integer-literal-equiv: Basic equivalence relation for dec-integer-literal structures.
Make-dec-integer-literal: Basic constructor macro for dec-integer-literal structures.
Dec-integer-literal->digits/uscores: Get the digits/uscores field from a dec-integer-literal.
Dec-integer-literal->suffix?: Get the suffix? field from a dec-integer-literal.
Change-dec-integer-literal: Modifying constructor for dec-integer-literal structures.
Dec-integer-literalp: Recognizer for dec-integer-literal structures.