		Search-engine friendly clone of the ACL2 documentation.

Octal-integer-literals

Oct-integer-literal

Fixtype of octal integer literals.

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

Fields

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

Additional Requirements

The following invariant is enforced on the fields:

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

An octal integer literal consists of (i) a sequence of octal digits and underscores satisfying the constraints in octdig/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 octal-integer-literal. This remains to be proved formally.

Subtopics

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