Enum LeanType 

pub enum LeanType {
    Prop,
    Type,
    Sort,
    Arrow(Box<LeanType>, Box<LeanType>),
    Named(String),
    App(Box<LeanType>, Vec<LeanType>),
}

Lean 4 type representation.

Variants

Prop

Prop

Type

Type universe

Sort

Sort universe

Arrow(Box<LeanType>, Box<LeanType>)

Function type (A → B)

Named(String)

Named type

App(Box<LeanType>, Vec<LeanType>)

Type application

Implementations

impl LeanType

pub fn to_lean(&self) -> String

Convert type to Lean 4 syntax

Trait Implementations

impl Clone for LeanType

fn clone(&self) -> LeanType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanType

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

Formats the value using the given formatter.