Struct Lean4Inductive 

pub struct Lean4Inductive {
    pub name: String,
    pub type_params: Vec<(String, Lean4Type)>,
    pub indices: Vec<Lean4Type>,
    pub constructors: Vec<Lean4Constructor>,
    pub derives: Vec<String>,
    pub doc_comment: Option<String>,
}

A Lean 4 inductive type declaration.

Fields

name: String

Type name

type_params: Vec<(String, Lean4Type)>

Type parameters: (α : Type u)

indices: Vec<Lean4Type>

Index types (GADTs)

constructors: Vec<Lean4Constructor>

Constructors

derives: Vec<String>

Derives (e.g., Repr, DecidableEq, BEq)

doc_comment: Option<String>

Optional doc comment

Implementations

impl Lean4Inductive

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

Create a simple inductive type.

pub fn emit(&self) -> String

Emit the inductive as Lean 4 source.

Trait Implementations

impl Clone for Lean4Inductive

fn clone(&self) -> Lean4Inductive

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Inductive

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

Formats the value using the given formatter.