Zulip Chat Archive

Stream: lean4

Topic: panic in macro_rules attributes


view this post on Zulip Mario Carneiro (Apr 12 2021 at 10:26):

@[simp] macro_rules | `(_) => `(_)

besides the normal errors, there is also a (not very specific) panic:

PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none

view this post on Zulip Mario Carneiro (Apr 12 2021 at 10:26):

you get this error regardless of the attribute

view this post on Zulip Daniel Selsam (Apr 12 2021 at 16:07):

This one doesn't panic any more, presumably because of https://github.com/leanprover/lean4/commit/83b83f51e99f725ec60d63b6e497d372b40c9fa6


Last updated: May 18 2021 at 23:14 UTC