Zulip Chat Archive

Stream: general

Topic: itactic in lean.parser


view this post on Zulip 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?

view this post on Zulip Keeley Hoek (Nov 22 2018 at 04:06):

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

view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Nov 22 2018 at 10:18):

</3 Heartbreaking but good to know, thanks Sebastian

view this post on Zulip Kevin Buzzard (Nov 22 2018 at 10:32):

And Lean 4?

view this post on Zulip 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