lean-to-dot-net
Lean to .NET
Prove a function in Lean 4, call it from C#. lean2il re-checks every proof with
Tenet, an independent Lean kernel, compiles the definitions you mark to
.NET IL, and writes their documentation from the Lean.
- Tutorial: from nothing to a proved Lean function called from C#, in about fifteen minutes.
- Guide: what Lean and Tenet are, every option, what compiles, how types map, what each error means.
- Finance.Proven API docs: the demo assembly’s docs, generated entirely from the Lean.
- The proofs in LeanViz: every declaration, browsable, re-checked by Tenet.
- Source on GitHub, MIT.