Struct Lean4Structure 

pub struct Lean4Structure {
    pub name: String,
    pub type_params: Vec<(String, Lean4Type)>,
    pub extends: Vec<String>,
    pub fields: Vec<(String, Lean4Type, Option<Lean4Expr>)>,
    pub doc_comment: Option<String>,
    pub derives: Vec<String>,
}

A Lean 4 structure declaration.

Fields

name: String

Structure name

type_params: Vec<(String, Lean4Type)>

Type parameters

extends: Vec<String>

Parent structures (extends)

fields: Vec<(String, Lean4Type, Option<Lean4Expr>)>

Fields: (name, type, default_value)

doc_comment: Option<String>

Optional doc comment

derives: Vec<String>

Derives

Implementations

impl Lean4Structure

pub fn simple(name: impl Into<String>, fields: Vec<(String, Lean4Type)>) -> Self

Create a simple structure.

pub fn emit(&self) -> String

Emit the structure as Lean 4 source.

Trait Implementations

impl Clone for Lean4Structure

fn clone(&self) -> Lean4Structure

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Structure

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

Formats the value using the given formatter.