Struct Lean4Def 

pub struct Lean4Def {
    pub name: String,
    pub type_params: Vec<(String, String)>,
    pub args: Vec<(String, Lean4Type)>,
    pub type_ascription: Option<Lean4Type>,
    pub body: Lean4Expr,
    pub doc_comment: Option<String>,
    pub attributes: Vec<String>,
    pub is_noncomputable: bool,
    pub is_private: bool,
}

A Lean 4 def definition.

Fields

name: String

Name of the definition

type_params: Vec<(String, String)>

Universe-polymorphic type parameters: {u v : Type}

args: Vec<(String, Lean4Type)>

Term-level arguments: (x : Nat) (y : Bool)

type_ascription: Option<Lean4Type>

Return type ascription

body: Lean4Expr

Body expression

doc_comment: Option<String>

Optional doc comment

attributes: Vec<String>

Lean attributes: @[simp], @[inline], etc.

is_noncomputable: bool

noncomputable

is_private: bool

private

Implementations

impl Lean4Def

pub fn simple( name: impl Into<String>, args: Vec<(String, Lean4Type)>, ret_ty: Lean4Type, body: Lean4Expr, ) -> Self

Create a simple definition.

pub fn emit(&self) -> String

Emit the definition as Lean 4 source.

Trait Implementations

impl Clone for Lean4Def

fn clone(&self) -> Lean4Def

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Def

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

Formats the value using the given formatter.