Examples of usage of Lean.Parser.Basic

Stream: general

[Ayhon]

Hello :wave:

I'm trying to solve this year's Advent of Code problems in Lean to practice a bit. Since I knew that Advent of Code problems many times require that you implement a parser (for instance, this year's Day 3), I wanted to look into idiomatic ways of doing so in Lean. That's when I came accross Lean.Parser.Basic, which seems to do what I want.

I've found the documentation a bit hard to follow, and was looking for some examples which could hopefully help me understand the contexts of some definitions. However, I didn't come up with anything while searching online. Does anyone have any good examples on how Lean.Parser.Basic is supposed to be used? How do you create a parser, and how do you run it?

[Edward van de Meent]

this is the parser lean uses to parse leans language (which is extensible, hence why this type exists). i suspect that it will be more useful/intuitive if you use docs#Std.Internal.Parsec ,although documentation for that is also not overflowing

[Ayhon]

Is it similar to the haskell library of the same name? If so I can just look to their documentation and try to translate the concepts

[Edward van de Meent]

somewhat, although i believe they are implemented differently internally

[nrs]

wrt to the original question you might be interested in
this zulip thread: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20get.20.60Syntax.60.20from.20string
and this discord message: https://discord.com/channels/1154493176548184134/1312024651701948446/1313509374182035506

[François G. Dorais]

For more flexibility, you can use https://github.com/fgdorais/lean4-parser