Lean 4 / Parser

A parser combinator library for Lean 4.


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.


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.