Struct Lean4Instance 

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

A Lean 4 instance declaration.

Fields

name: Option<String>

Optional instance name

ty: Lean4Type

Type class application (the type being instantiated)

args: Vec<(String, Lean4Type)>

Arguments (implicit, typeclass)

body: Lean4Expr

The instance body (a where block or a term)

Implementations

impl Lean4Instance

pub fn emit(&self) -> String

Emit the instance as Lean 4 source.

Trait Implementations

impl Clone for Lean4Instance

fn clone(&self) -> Lean4Instance

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Instance

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

Formats the value using the given formatter.