		Search-engine friendly clone of the ACL2 documentation.

Hexadecimal-integer-literals

Hex-integer-literal

Fixtype of hexadecimal integer literals.

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

Fields

digits/uscores — hexdig/uscore-list
prefix-upcase-p — booleanp
suffix? — optional-integer-type-suffix

Additional Requirements

The following invariant is enforced on the fields:

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

A hexadecimal integer literal consist of (i) a lowercase or uppercase prefix, (ii) a sequence of hexadecimal digits and underscores satisfying the constraints in hexdig/uscore-list-wfp, and (iii) 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 hex-integer-literal. This remains to be proved formally.

Subtopics

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