Lean 4 / Parser

A parser combinator library for Lean 4.

Installation

Add this dependency to your project's lakefile.lean:

require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"

Then add import Parser at the top of any Lean file where you plan to use this library.

Acknowledgements

Original work for the Lean 4 Parser library was done by François G. Dorais, Kyrill Serdyuk, and Emma Shroyer. This work was partly supported by the CEMS REU program at The University of Vermont.

---

• The Parser library is copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. The library is released under the Apache 2.0 license. See the file LICENSE for additional details.