# Tree-Sitter-Lean4
Language bindings for Rust programs to parse [Lean 4](github.com/leanprover/lean4) source code. Lean4 is a programming language, commonly used for mathematical theorem proving as a [proof assistant](https://en.wikipedia.org/wiki/Proof_assistant).
## Installation
Add this crate as a normal dependency in your `Cargo.toml` file.
The parser is automatically generated by the build script in [`build.rs`](./build.rs) if it is missing. This requires `tree-sitter` and a C compiler installed.
## Usage
See [Tree-Sitter-Rust](https://github.com/tree-sitter/tree-sitter/tree/master/lib/binding_rust).
**Important**: Lean is a very extensible language. Therefore, the Tree-Sitter grammar is of limited use. For parsing advanced Lean programs you will need to use the Lean kernel. See also [Metaprogramming in Lean](https://github.com/leanprover-community/lean4-metaprogramming-book).
## Development
Based on <https://github.com/Julian/lean.nvim>.
## License
MIT