Zulip Chat Archive

Stream: new members

Topic: How to get Subtypes to inherit typeclasses


view this post on Zulip Jem Bishop (Nov 05 2020 at 16:31):

Hi! I want to create a subtype of the natural numbers less than or equal to 5. With
def House := {n : ℕ // n ≤ 5}
this seems to lose all the typeclass instances the natural numbers have, (I can't add or use = with nats) ! How do I get them for this subtype? Thanks!

view this post on Zulip Johan Commelin (Nov 05 2020 at 16:33):

@Jem Bishop What is 4 + 4 in this type?

view this post on Zulip Johan Commelin (Nov 05 2020 at 16:33):

Note that mathlib has fin 6 and zmod 6 which are two types that have the same definition as House but are equipped with a bunch of typeclass instances.

view this post on Zulip Jem Bishop (Nov 05 2020 at 16:35):

I see, thanks for your help!

view this post on Zulip Jem Bishop (Nov 05 2020 at 16:40):

In this case I would like 4 + 4 = 5, so I guess I would create these instances for add on fin manually

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 21:15):

(deleted)


Last updated: May 11 2021 at 13:22 UTC