Top

Literals

Literal

Fixtype of literals.

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

Member Tags → Types

:integer → literal-integer
:fpoint → literal-fpoint
:char → literal-char
:string → literal-string
:boolean → literal-boolean
:null → literal-null

This corresponds to the grammar rule for literal [JLS14:3.10].

Note that we just use the built-in ACL2 booleans for the boolean literals, since they are so simple.

Subtopics

Literal-case: Case macro for the different kinds of literal structures.
Literal-fix: Fixing function for literal structures.
Literal-equiv: Basic equivalence relation for literal structures.
Literalp: Recognizer for literal structures.
Literal-string
Literal-integer
Literal-fpoint
Literal-char
Literal-boolean
Literal-kind: Get the kind (tag) of a literal structure.
Literal-null