Zulip Chat Archive

Stream: general

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 finite s.

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 set.finite.

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