Open sacerdot opened 1 month ago
Mildly related: I just leaned that panics are not visible on https://live.lean-lang.org/. I sometimes wonder if panics within commands couldn’t be somehow caught and turned into error, with a location etc.
Anyways, the panic message here is
PANIC at Lean.Elab.Tactic.SolveByElim.parseArgs Lean.Elab.Tactic.SolveByElim:45:11: Unreachable parse of solve_by_elim arguments.
and it can be reproduced on current master
.
Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
In macro_rules, the (`tactic|...) quotation allows to concatenate a possibly empty list with a single element putting a separator in the middle. When the rule is triggered on an empty list, the result is a singleton list that starts with the separator, leading to some panic in tactic code. The following is a minimal example:
Steps to Reproduce
Run the code above. The last line triggers the panic
Versions
4.9.0-rc3