Struct Lean4Backend 

pub struct Lean4Backend { /* private fields */ }

Lean 4 code generation backend.

Implementations

impl Lean4Backend

pub fn new() -> Self

Create a new Lean 4 backend.

pub fn with_std_imports() -> Self

Create a backend with standard Lean 4 imports.

pub fn compile_kernel_decl( &mut self, name: &str, args: Vec<(String, Lean4Type)>, ret_ty: Lean4Type, body: Lean4Expr, )

Compile a simple kernel declaration (name + type + body) to a Lean 4 def.

pub fn add_theorem( &mut self, name: &str, args: Vec<(String, Lean4Type)>, ty: Lean4Type, tactics: Vec<String>, )

Add a theorem with a tactic proof.

pub fn add_inductive(&mut self, ind: Lean4Inductive)

Add an inductive type.

pub fn emit_file(&self) -> String

Emit the complete Lean 4 file.

pub fn file_mut(&mut self) -> &mut Lean4File

Get a mutable reference to the file.

Trait Implementations

impl Default for Lean4Backend

fn default() -> Self

Returns the “default value” for a type.