Enum Lean4Expr 

pub enum Lean4Expr {
    Var(String),
    NatLit(u64),
    IntLit(i64),
    BoolLit(bool),
    StrLit(String),
    FloatLit(f64),
    Hole,
    Sorry,
    Panic(String),
    App(Box<Lean4Expr>, Box<Lean4Expr>),
    Lambda(String, Option<Box<Lean4Type>>, Box<Lean4Expr>),
    Pi(String, Box<Lean4Type>, Box<Lean4Expr>),
    Let(String, Option<Box<Lean4Type>>, Box<Lean4Expr>, Box<Lean4Expr>),
    LetRec(String, Box<Lean4Expr>, Box<Lean4Expr>),
    Match(Box<Lean4Expr>, Vec<(Lean4Pattern, Lean4Expr)>),
    If(Box<Lean4Expr>, Box<Lean4Expr>, Box<Lean4Expr>),
    Do(Vec<Lean4DoStmt>),
    Have(String, Box<Lean4Type>, Box<Lean4Expr>, Box<Lean4Expr>),
    Show(Box<Lean4Type>, Box<Lean4Expr>),
    Calc(Vec<Lean4CalcStep>),
    ByTactic(Vec<String>),
    Ascription(Box<Lean4Expr>, Box<Lean4Type>),
    Tuple(Vec<Lean4Expr>),
    AnonymousCtor(Vec<Lean4Expr>),
    Proj(Box<Lean4Expr>, String),
    StructLit(String, Vec<(String, Lean4Expr)>),
}

Lean 4 expression representation.

Variants

Var(String)

Variable reference: x

NatLit(u64)

Natural number literal: 42

IntLit(i64)

Integer literal: -5

BoolLit(bool)

Boolean literal: true / false

StrLit(String)

String literal: "hello"

FloatLit(f64)

Float literal: 3.14

Hole

Hole / sorry placeholder: _

Sorry

sorry

Panic(String)

Panic: panic! "message"

App(Box<Lean4Expr>, Box<Lean4Expr>)

Function application: f x

Lambda(String, Option<Box<Lean4Type>>, Box<Lean4Expr>)

Lambda: fun x => body

Pi(String, Box<Lean4Type>, Box<Lean4Expr>)

Dependent function type (Pi): (x : α) → β x

Let(String, Option<Box<Lean4Type>>, Box<Lean4Expr>, Box<Lean4Expr>)

Let binding: let x := e; body

LetRec(String, Box<Lean4Expr>, Box<Lean4Expr>)

Recursive let: let rec f := ...

Match(Box<Lean4Expr>, Vec<(Lean4Pattern, Lean4Expr)>)

Pattern match: match e with | p => b | ...

If(Box<Lean4Expr>, Box<Lean4Expr>, Box<Lean4Expr>)

If-then-else: if c then t else e

Do(Vec<Lean4DoStmt>)

Do notation block

Have(String, Box<Lean4Type>, Box<Lean4Expr>, Box<Lean4Expr>)

have h : T := proof; rest

Show(Box<Lean4Type>, Box<Lean4Expr>)

show T from e

Calc(Vec<Lean4CalcStep>)

Calc block

ByTactic(Vec<String>)

Tactic block: by tac1; tac2; ...

Ascription(Box<Lean4Expr>, Box<Lean4Type>)

Type ascription: (e : T)

Tuple(Vec<Lean4Expr>)

Tuple: (a, b)

AnonymousCtor(Vec<Lean4Expr>)

Anonymous constructor: ⟨a, b⟩

Proj(Box<Lean4Expr>, String)

Projection: e.1, e.field

StructLit(String, Vec<(String, Lean4Expr)>)

Structure literal: { field := val, ... }

Trait Implementations

impl Clone for Lean4Expr

fn clone(&self) -> Lean4Expr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Expr

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

Formats the value using the given formatter.

impl Display for Lean4Expr

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

Formats the value using the given formatter.

impl PartialEq for Lean4Expr

fn eq(&self, other: &Lean4Expr) -> 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 StructuralPartialEq for Lean4Expr