Zulip Chat Archive

Stream: lean4

Topic: tactic1 <|> tactic2

David Renshaw (Jul 16 2022 at 20:48):

The metaprogramming book claims that <|> is a tactic combinator such that

t <|> u first executes t. If t fails, it backtracks and executes u

(https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/c79bc6a8f0be11045ed8b25f253709c8e440f275/lean/main/metam.lean#L1113)

However, as far as I can tell, this only works in Lean 3, not in Lean 4. I ended up defining my own similar syntax for lean4-maze: https://github.com/dwrensha/lean4-maze/blob/45838fde6580d6be0252a91c649afa1398a62068/Maze.lean#L271-L274

Am I missing something here?

Arthur Paulino (Jul 16 2022 at 20:53):

That part of the book is indeed needing a revamp. Here's another issue: https://github.com/arthurpaulino/lean4-metaprogramming-book/issues/49

Arthur Paulino (Jul 16 2022 at 20:54):

Feel free to open an issue or even a PR :D
I'll take a look when I get home

Sebastian Ullrich (Jul 16 2022 at 20:55):

<|> is correct on the monadic level. There is docs4#Lean.Parser.Tactic.first on the tactic DSL level.

David Renshaw (Jul 16 2022 at 21:12):

Opened https://github.com/arthurpaulino/lean4-metaprogramming-book/pull/63.

Arthur Paulino (Jul 16 2022 at 22:06):

Wait, I had linked something unrelated :sweat_smile:

Arthur Paulino (Jul 16 2022 at 22:06):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC