Total parser combinators for Lean4

Stream: general

[Remi]

Introduce leansec - total parser combinators library, that can be used to quickly prototype complex grammar parsers without worrying about totality.

No documentation yet, but there’s one example of arithmetic language from the original paper.

I’ve used agdarsec original paper and parseque (port to Coq) as my primary references, so some of the abstractness can lack for now. But I plan to fix it, for example abstract over token type.

Suggestions are welcome!