Closed dwrensha closed 2 years ago
t <|> u does not exist in Lean 4 at a tactic level. (It does exist as a monadic combinator.)
t <|> u
See https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html#Lean.Parser.Tactic.first
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/tactic1.20.3C.7C.3E.20tactic2/near/289847287
t <|> udoes not exist in Lean 4 at a tactic level. (It does exist as a monadic combinator.)See https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html#Lean.Parser.Tactic.first
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/tactic1.20.3C.7C.3E.20tactic2/near/289847287