Topic: Finite sets/types docs
Johan Commelin (Aug 24 2022 at 08:13):
Mental note: we should update https://leanprover-community.github.io/theories/sets.html now that the
finite typeclass exists.
Chris Hughes (Aug 24 2022 at 20:04):
I think I wrote that a very long time ago. I didn't understand Lean that well at the time, so I think it might not be the most helpful anyway.
Wrenna Robson (Aug 24 2022 at 22:58):
It is slightly counterintuitive that the definition of
set.finite s is not
Kyle Miller (Aug 24 2022 at 23:07):
@Wrenna Robson It's that way because
finite is newer. I believe @Yury G. Kudryashov has a PR somewhere that updates
Wrenna Robson (Aug 24 2022 at 23:08):
Right, when I spoke to Yaël about it earlier today they made it sound like it would be staying as it is.
Yaël Dillies (Aug 25 2022 at 07:15):
I thought we wouldn't switch to that definition because that would make
set.finite a class, hence frozen in the local context.
Last updated: Aug 03 2023 at 10:10 UTC