## Stream: general

### Topic: itactic in lean.parser

#### Keeley Hoek (Nov 22 2018 at 04:05):

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 (Nov 22 2018 at 04:06):

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

#### Sebastian Ullrich (Nov 22 2018 at 09:05):

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 (Nov 22 2018 at 10:18):

</3 Heartbreaking but good to know, thanks Sebastian

And Lean 4?

#### Sebastian Ullrich (Nov 22 2018 at 14:43):

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

Last updated: May 16 2021 at 05:21 UTC