Stream: general

Topic: finite set lemmas very hard to use

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?

Kevin Buzzard (May 27 2018 at 17:02):

You mean instead of using the type class resolution system?

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

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

Kevin Buzzard (May 27 2018 at 17:04):

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