Zulip Chat Archive

Stream: general

Topic: instance brackets right of the colon in meta definitions


view this post on Zulip Chris Hughes (Aug 16 2020 at 09:19):

This code makes an error, but works if I make the instance brackets into explicit brackets, or remove the meta. Is this a bug?

meta def f : Π {α : Type} [h : decidable_eq α], nat := sorry

view this post on Zulip Kenny Lau (Aug 16 2020 at 10:11):

another reason to prefer the better implicit brackets:

meta def f : Π α : Type [h : decidable_eq α], nat := sorry

view this post on Zulip Yury G. Kudryashov (Aug 17 2020 at 14:30):

But there is no next explicit argument


Last updated: May 15 2021 at 23:13 UTC