Module lean 

Enums

RecursionPlan

Proof-mode recursion support class for emitted Lean definitions.

VerifyEmitMode

How verify blocks should be emitted in generated Lean.

Functions

proof_mode_issues

Strict proof-mode gate for Lean transpilation.

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.