Zulip Chat Archive

Stream: new members

Topic: Understanding Set and finset better


ROCKY KAMEN-RUBIO (Jun 18 2020 at 20:34):

Has anyone written any tutorials on sets and finsets/fintypes/nodeup/card? I'm having trouble understanding what's going on just from the documentation.

Patrick Massot (Jun 18 2020 at 20:39):

we have https://leanprover-community.github.io/theories/sets.html

Bhavik Mehta (Jun 18 2020 at 20:54):

If your goal is to use finsets, fintype and card, I'd suggest looking at the theorem statements in data.finset and data.fintype, and totally ignoring nodup

Bhavik Mehta (Jun 18 2020 at 20:55):

There's a very thorough finset API (albeit not the best documented) but at no point should you need to worry about how a finset is actually implemented

ROCKY KAMEN-RUBIO (Jun 19 2020 at 00:28):

Bhavik Mehta said:

There's a very thorough finset API (albeit not the best documented) but at no point should you need to worry about how a finset is actually implemented

That's good to know. A lot of my confusion was coming from the implementation so I'll try ignoring that and see if I can make better sense of it.


Last updated: Dec 20 2023 at 11:08 UTC