Module lean 

Re-exports

pub use crate::codegen::recursion::ProofModeIssue;

pub use crate::codegen::recursion::RecursionPlan;

Enums

VerifyEmitMode

How verify blocks should be emitted in generated Lean.

Functions

proof_mode_findings

Proof-mode diagnostics for Lean transpilation.

proof_mode_issues

transpile

Transpile an Aver program to a Lean 4 project.

transpile_for_proof_mode

Proof-mode transpilation.

transpile_with_verify_mode

Transpile an Aver program to a Lean 4 project with configurable verify proof mode.