Enum Lean4Type 

pub enum Lean4Type {
    Nat,
    Int,
    Float,
    Bool,
    String,
    Unit,
    Prop,
    Type(u32),
    List(Box<Lean4Type>),
    Option(Box<Lean4Type>),
    Prod(Box<Lean4Type>, Box<Lean4Type>),
    Sum(Box<Lean4Type>, Box<Lean4Type>),
    Fun(Box<Lean4Type>, Box<Lean4Type>),
    Custom(String),
    ForAll(String, Box<Lean4Type>, Box<Lean4Type>),
    App(Box<Lean4Type>, Box<Lean4Type>),
    IO(Box<Lean4Type>),
    Array(Box<Lean4Type>),
    Fin(Box<Lean4Type>),
    Char,
}

Lean 4 type representation.

Variants

Nat

Nat — natural numbers

Int

Int — integers

Float

Float — 64-bit floating point

Bool

Bool — boolean

String

String — string type

Unit

Unit — unit type

Prop

Prop — sort of propositions

Type(u32)

Type u — universe

List(Box<Lean4Type>)

List α

Option(Box<Lean4Type>)

Option α

Prod(Box<Lean4Type>, Box<Lean4Type>)

α × β (product)

Sum(Box<Lean4Type>, Box<Lean4Type>)

α ⊕ β (sum / Either)

Fun(Box<Lean4Type>, Box<Lean4Type>)

α → β (function type)

Custom(String)

Named type (user-defined or imported)

ForAll(String, Box<Lean4Type>, Box<Lean4Type>)

∀ (x : α), β x (dependent function / Pi type)

App(Box<Lean4Type>, Box<Lean4Type>)

Type application: f α

IO(Box<Lean4Type>)

IO α

Array(Box<Lean4Type>)

Array α

Fin(Box<Lean4Type>)

Fin n

Char

Char

Trait Implementations

impl Clone for Lean4Type

fn clone(&self) -> Lean4Type

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Type

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

Formats the value using the given formatter.

impl Display for Lean4Type

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

Formats the value using the given formatter.

impl Hash for Lean4Type

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 Lean4Type

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Lean4Type

impl StructuralPartialEq for Lean4Type