		Search-engine friendly clone of the ACL2 documentation.

Literals

Literal

Fixtype of Leo literals.

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

Integer literals are typed. They are unsigned or signed, and they have a bit size. The value is always a natural number; negative integers are represented as unary negations of signed literals.

String literals consist of lists of characters. Currently there is no character literal but we continue to use char to represent string elements.

Field literals represent elements of the field type, which are natural numbers below the base prime. We allow any natural number here, which denotes the field element obtained by reducing modulo the prime.

Group literals are described in group-literal.

Scalar literals represent elements of the scalar type, which are natural numbers below the scalar prime. We allow any natural number here, which denotes the field element obtained by reducing modulo the prime.

Subtopics

Literal-fix: Fixing function for literal structures.
Literal-case: Case macro for the different kinds of literal structures.
Literalp: Recognizer for literal structures.
Literal-equiv: Basic equivalence relation for literal structures.
Literal-unsigned
Literal-signed
Literal-string
Literal-group
Literal-bool
Literal-address
Literal-scalar
Literal-field
Literal-kind: Get the kind (tag) of a literal structure.

Literal

Member Tags → Types

Subtopics