Struct Lean4Abbrev 

pub struct Lean4Abbrev {
    pub name: String,
    pub args: Vec<(String, Lean4Type)>,
    pub ty: Option<Lean4Type>,
    pub body: Lean4Expr,
}

A Lean 4 abbrev declaration (transparent definition).

Fields

name: String

Name

args: Vec<(String, Lean4Type)>

Arguments

ty: Option<Lean4Type>

Return type

body: Lean4Expr

Body

Implementations

impl Lean4Abbrev

pub fn emit(&self) -> String

Emit the abbrev as Lean 4 source.

Trait Implementations

impl Clone for Lean4Abbrev

fn clone(&self) -> Lean4Abbrev

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Abbrev

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

Formats the value using the given formatter.