Struct Lean4Axiom 

pub struct Lean4Axiom {
    pub name: String,
    pub args: Vec<(String, Lean4Type)>,
    pub ty: Lean4Type,
    pub doc_comment: Option<String>,
}

A Lean 4 axiom declaration.

Fields

name: String

Axiom name

args: Vec<(String, Lean4Type)>

Arguments

ty: Lean4Type

The type (proposition)

doc_comment: Option<String>

Optional doc comment

Implementations

impl Lean4Axiom

pub fn emit(&self) -> String

Emit the axiom as Lean 4 source.

Trait Implementations

impl Clone for Lean4Axiom

fn clone(&self) -> Lean4Axiom

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4Axiom

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

Formats the value using the given formatter.