Zulip Chat Archive

Stream: lean4

Topic: panic in quotation parsing


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

view this post on Zulip 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: May 07 2021 at 12:15 UTC