nanoda_lib

nanoda_lib is a Rust library providing type inference and checking for the Lean 4 theorem prover.

nanoda_lib is a Rust-based library that implements type inference and checking functionalities for the Lean 4 programming language and theorem prover. It serves as an external type checker, offering a robust solution for verifying Lean 4 code. The library integrates as a standard Rust crate, configured via a JSON file for modern development workflows, including CI and automation. Its design prioritizes flexibility and aims to support the evolving landscape of external type checkers for Lean 4.

https://github.com/ammkrn/nanoda_lib