Enum LeanProofTerm 

pub enum LeanProofTerm {
    Var(String),
    App {
        function: Box<LeanProofTerm>,
        args: Vec<LeanProofTerm>,
    },
    Lambda {
        params: Vec<(String, LeanType)>,
        body: Box<LeanProofTerm>,
    },
    Tactic(LeanTactic),
    Have {
        name: String,
        ty: Option<LeanType>,
        proof: Box<LeanProofTerm>,
        body: Box<LeanProofTerm>,
    },
}

A Lean 4 proof term.

Variants

Var(String)

Variable reference

App

Function application

Fields

function: Box<LeanProofTerm>

args: Vec<LeanProofTerm>

Lambda

Lambda abstraction

Fields

params: Vec<(String, LeanType)>

body: Box<LeanProofTerm>

Tactic(LeanTactic)

Tactic proof

Have

Have statement

Fields

name: String

ty: Option<LeanType>

proof: Box<LeanProofTerm>

body: Box<LeanProofTerm>

Implementations

impl LeanProofTerm

pub fn to_lean(&self) -> String

Convert proof term to Lean 4 syntax

Trait Implementations

impl Clone for LeanProofTerm

fn clone(&self) -> LeanProofTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanProofTerm

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

Formats the value using the given formatter.