pub enum Literal {
Int(i64),
Float(f64),
Text(String),
Duration(i64),
Date(i32),
Moment(i64),
BigInt(BigInt),
Nat(BigInt),
}Expand description
Primitive literal values.
These are opaque values that compute via hardware ALU, not recursion.
Variants§
Int(i64)
64-bit signed integer
Float(f64)
64-bit floating point
Text(String)
UTF-8 string
Duration(i64)
Duration in nanoseconds (signed for negative offsets like “5 min early”)
Date(i32)
Calendar date as days since Unix epoch (i32 gives ±5.8 million year range)
Moment(i64)
Instant in time as nanoseconds since Unix epoch (UTC)
BigInt(BigInt)
Arbitrary-precision integer — the Int values that overflow i64 (K6). This is a
PARALLEL representation, appended so existing certificates’ Int/Float/… encoding
is byte-unchanged. A BigInt is CANONICAL: it holds only values to_i64() cannot,
so every integer has a unique Literal (small → Int, huge → BigInt) and
definitional equality stays sound. Serialized as a decimal string, stable across
BigInt’s internal limb layout. Produced by int_lit; never constructed directly
for a value that fits i64.
Nat(BigInt)
Arbitrary-precision NATURAL-number literal — a compact, accelerated form of the
unary Peano numeral Succ^n Zero (K6). Nat(n) is DEFINITIONALLY EQUAL to Succ
applied n times to Zero: the kernel bridges the two in extract_constructor
(so a match/recursor computes on it, peeling one Succ per step) and in def_eq
(so Nat(n) and Succ^n Zero are interchangeable), in BOTH kernels. It stores the
count as one BigInt instead of n heap nodes. Serialized as a decimal string;
the value is non-negative.