itactic in lean.parser

Stream: general

[Keeley Hoek]

Inside a lean.parser monad, I can for example read a name by

n <- ident

Is there any way to do the same thing with an itactic block? i.e. expecting a begin ... end or { ... } block?

[Keeley Hoek]

In the end, I'm trying to make a command which _optionally_ accepts an itactic block

[Sebastian Ullrich]

Unfortunately no. itactic is not a parser in Lean 3 for technical reasons and can only be used directly as a parameter type.

[Keeley Hoek]

</3 Heartbreaking but good to know, thanks Sebastian

[Kevin Buzzard]

And Lean 4?

[Sebastian Ullrich]

There will be some itactic parser in Lean 4 since all parsing will be done in Lean, and you should be able to reuse it to you heart's content