Enum Lean4Decl 

pub enum Lean4Decl {
    Def(Lean4Def),
    Theorem(Lean4Theorem),
    Axiom(Lean4Axiom),
    Abbrev(Lean4Abbrev),
    Structure(Lean4Structure),
    Inductive(Lean4Inductive),
    Instance(Lean4Instance),
    Check(Lean4Expr),
    Eval(Lean4Expr),
    Raw(String),
    Section(String, Vec<Lean4Decl>),
    Namespace(String, Vec<Lean4Decl>),
}

Top-level Lean 4 declaration.

Variants

Def(Lean4Def)

def definition

Theorem(Lean4Theorem)

theorem declaration

Axiom(Lean4Axiom)

axiom declaration

Abbrev(Lean4Abbrev)

abbrev declaration

Structure(Lean4Structure)

structure declaration

Inductive(Lean4Inductive)

inductive type

Instance(Lean4Instance)

instance declaration

Check(Lean4Expr)

#check command

Eval(Lean4Expr)

#eval command

Raw(String)

Raw source string (escape hatch)

Section(String, Vec<Lean4Decl>)

Section: section Name ... end Name

Namespace(String, Vec<Lean4Decl>)

Namespace: namespace Name ... end Name

Implementations

impl Lean4Decl

pub fn emit(&self) -> String

Emit the declaration as Lean 4 source.

Trait Implementations

impl Clone for Lean4Decl

fn clone(&self) -> Lean4Decl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Decl

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

Formats the value using the given formatter.