Zulip Chat Archive

Stream: lean4

Topic: panic in quotation parsing

Mario Carneiro (Apr 12 2021 at 15:04):

#eval `([x,])
-- PANIC at _private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.quoteSyntax Lean.Elab.Quotation:130:22: unreachable code has been reached

Daniel Selsam (Apr 12 2021 at 16:08):

This one triggers the same line as https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unreachable.20code.20panic I will post a GitHub issue for this pair

Last updated: Dec 20 2023 at 11:08 UTC