		Search-engine friendly clone of the ACL2 documentation.

Binary-integer-literals

Bin-integer-literal

Fixtype of binary integer literals.

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

Fields

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

Additional Requirements

The following invariant is enforced on the fields:

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

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

Subtopics

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