Struct LeanExporter 

pub struct LeanExporter { /* private fields */ }

Lean proof exporter (Lean 4 format)

Implementations

impl LeanExporter

pub fn new() -> Self

Create a new Lean exporter (defaults to Lean 4)

pub fn lean3() -> Self

Create a Lean 3 exporter

pub fn export_proof(&mut self, proof: &Proof) -> String

Export a proof to Lean format

pub fn export_theory_proof(&mut self, theory_proof: &TheoryProof) -> String

Export a theory proof to Lean format

Trait Implementations

impl Debug for LeanExporter

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

Formats the value using the given formatter.

impl Default for LeanExporter

fn default() -> Self

Returns the “default value” for a type.