Zulip Chat Archive

Stream: general

Topic: finite set lemmas very hard to use


view this post on Zulip Chris Hughes (May 27 2018 at 16:28):

A lot of the finite set lemmas are extremely difficult to use. For example set.empty_card can only be used in a rewrite, if I've used fintype_empty as my fintype instance in my goal. Would it be a good idea to make fintype instances an argument to the lemma whenever they're used in the statement of a theorem?

view this post on Zulip Kevin Buzzard (May 27 2018 at 17:02):

You mean instead of using the type class resolution system?

view this post on Zulip Kevin Buzzard (May 27 2018 at 17:02):

Let me just comment that if I've understood your question correctly then I had the same problems using the is_ring_hom typeclass and it seemed to me initially that by far the easiest fix was just to make it not a typeclass

view this post on Zulip Kevin Buzzard (May 27 2018 at 17:03):

but instead I started that typeclass woes thread, and every time I got stuck or frustrated, Mario explained how to do it

view this post on Zulip Kevin Buzzard (May 27 2018 at 17:04):

Actually on re-reading -- are you asking something else?

view this post on Zulip Mario Carneiro (May 27 2018 at 17:13):

The solution is to use that fintype is a subsingleton to fix your argument


Last updated: May 11 2021 at 12:15 UTC