Struct Lean4 

pub struct Lean4;

Marker for the Lean 4 backend.

Implementations

impl Lean4

pub fn export_module(module_name: &str, obligations: &[Obligation]) -> String

Export a list of obligations as a Lean 4 module skeleton.

pub fn export_module_with_prelude( module_name: &str, obligations: &[Obligation], prelude: LeanPrelude, ) -> String

Export a list of obligations as a Lean 4 module skeleton with explicit prelude metadata.

pub fn export(module_name: &str, obligations: &[Obligation]) -> LeanExport

Export a list of obligations as structured Lean metadata plus source.

pub fn export_with_prelude( module_name: &str, obligations: &[Obligation], prelude: LeanPrelude, ) -> LeanExport

Export a list of obligations as structured Lean metadata plus source with explicit prelude metadata.

pub fn export_bundle(module_name: &str, bundle: &ObligationBundle) -> String

Export a bundle of obligations as a Lean 4 module skeleton.

pub fn export_bundle_structured( module_name: &str, bundle: &ObligationBundle, ) -> LeanExport

Export a bundle of obligations as structured Lean metadata plus source.

pub fn project(export: &LeanExport) -> LeanProject

Derive Lean package metadata from a structured export.