Zulip Chat Archive
Stream: Is there code for X?
Topic: finset.has_coe_to_sort
Eric Wieser (Dec 11 2020 at 11:37):
Is there a coercion from finset to a X : Type* with fintype X?
Mario Carneiro (Dec 11 2020 at 11:38):
yes
Mario Carneiro (Dec 11 2020 at 11:40):
Mario Carneiro (Dec 11 2020 at 11:40):
it's a double coercion via set X
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.
Patrick Massot (Dec 11 2020 at 13:04):
Yes, it's a very common elaboration curse.
Yury G. Kudryashov (Dec 12 2020 at 18:43):
You can define a docs#has_coe_to_sort instance on finset.
Eric Wieser (Dec 12 2020 at 19:35):
Should mathlib do so?
Yury G. Kudryashov (Dec 12 2020 at 20:54):
I don't know.
Last updated: Dec 20 2023 at 11:08 UTC