Enum Literal 

pub enum Literal {
    Nat(BigNat),
    Str(String),
}

Literal values supported natively.

Exactly the two literal kinds of the Lean 4 kernel: arbitrary-precision natural numbers (natVal) and UTF-8 strings (strVal). There is deliberately no integer literal — Lean encodes integers as Int.ofNat / Int.negSucc over Nat literals, and a signed fixed-width literal inside the TCB previously carried wrapping arithmetic.

Variants

Nat(BigNat)

Natural number literal (arbitrary precision).

Str(String)

String literal.

Implementations

impl Literal

pub fn nat(n: u64) -> Self

Build a Nat literal from a small value (ergonomic constructor).

pub fn string(s: impl Into<String>) -> Self

Build a String literal.

pub fn is_nat(&self) -> bool

Return true if this is a natural number literal.

pub fn is_str(&self) -> bool

Return true if this is a string literal.

pub fn as_nat(&self) -> Option<u64>

Extract the natural number value if it fits in u64 (best effort; returns None for larger values — use Literal::as_bignat for the exact value).

pub fn as_bignat(&self) -> Option<&BigNat>

Extract the exact natural number value, or None.

pub fn as_str(&self) -> Option<&str>

Extract the string value, or None.

pub fn type_name(&self) -> &'static str

Return the Lean type name for this literal.

Trait Implementations

impl Clone for Literal

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Literal

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Literal

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Literal

impl From<BigNat> for Literal

fn from(n: BigNat) -> Self

Converts to this type from the input type.

impl From<u64> for Literal

fn from(n: u64) -> Self

Converts to this type from the input type.

impl Hash for Literal

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Literal

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Literal