Zulip Chat Archive

Stream: Is there code for X?

Topic: finset.has_coe_to_sort


view this post on Zulip Eric Wieser (Dec 11 2020 at 11:37):

Is there a coercion from finset to a X : Type* with fintype X?

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:38):

yes

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:40):

docs#finset_coe.fintype

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:40):

it's a double coercion via set X

view this post on Zulip Anne Baanen (Dec 11 2020 at 11:42):

It has very annoying notation though, you need to write out (↑s : set X) before the elaborator gets what's going on.

view this post on Zulip Patrick Massot (Dec 11 2020 at 13:04):

Yes, it's a very common elaboration curse.

view this post on Zulip Yury G. Kudryashov (Dec 12 2020 at 18:43):

You can define a docs#has_coe_to_sort instance on finset.

view this post on Zulip Eric Wieser (Dec 12 2020 at 19:35):

Should mathlib do so?

view this post on Zulip Yury G. Kudryashov (Dec 12 2020 at 20:54):

I don't know.


Last updated: May 17 2021 at 14:12 UTC