		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Iconst-length

Fixtype of lengths of integer constants [C17:6.4.4.1].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:none → iconst-length-none
:long → iconst-length-long
:llong → iconst-length-llong

An integer constant may have (i) an l or L suffix, or (ii) an ll or LL suffix, or (iii) no such suffix. This fixtype captures these three possibilities, without distinguishing between the lowercase and uppercase variants (given the similarity between `l' and `1' and `I' in many fonts, it could be argued that one should always use the uppercase variants, as recommended in the Java language specification for Java).

Since the grammar in [C17] refers to these as long-suffix and long-long-suffix, it seems appropriate to call these the `length' of an integer constant, which justifies the name of this fixtype.

Subtopics

Iconst-length-fix: Fixing function for iconst-length structures.
Iconst-length-case: Case macro for the different kinds of iconst-length structures.
Iconst-length-equiv: Basic equivalence relation for iconst-length structures.
Iconst-lengthp: Recognizer for iconst-length structures.
Iconst-length-none
Iconst-length-long
Iconst-length-llong
Iconst-length-kind: Get the kind (tag) of a iconst-length structure.