coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] typeclass substructure question

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] typeclass substructure question
Date: Wed, 20 May 2020 15:14:54 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f180.google.com
Ironport-phdr: 9a23:8EKgrRxQ5Bic/fvXCy+O+j09IxM/srCxBDY+r6Qd2uwTIJqq85mqBkHD//Il1AaPAdyGrasc2qGP6PiocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTqwbalvIBmqqQjdudQajIV+Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlTwKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8dZMCAeQBM+hGsofzpFkBrRW5CwajGOzhxSRFhmP00KAgz+gsCx3K0BImEtkTsHrUttL1NKIKXOy7zqnIyjPDb/JV2Tjj7IjHbA4urOqDXbJ1a8XRyE0vGxnZgVWXrIzpMS6e2+MPs2ic6epgVOGvhHAjqw5vvDei3cgsiozTiYIUzlDI7zl2wIEwJdChTkNwfNGrHodKuS6AK4t2Xt0tQ3tuuCsi1rELtoO3cDUUxZknxBPSaPOKfpaG7B/sWuicLzl1iGxrdb+/mhu/7Eiux+PhWsSq3lhHsClInNfIu34N1xLe6c6KQeZ+8Ee5wTuDyRzf5+VeLU03lafXMYMtz78smpYJrEjOHTP6lF3ogKKXakko5+2l5/njb7r6o5KROI55hh3iPqkrhMCwGuo4PRULUmeF5euzyb3u8EjnT7hJgP02nKzUsJ7EKssFuKG0BgBY3Zgi5hmiCTqtzc4WkmMdLF1ffRKKl4jpNE/KIPD/Ffq/hk6jkDZvx/zfJ73hHojBImHNkLv8frtx91RQyAU0zdBY6JJUDq8OLOjvVU/2sdzUFh45MwqqzOb7ENhxyJ8SVGaVDqKaMK7eq0KE6+MzL+WWeYMYuyrxJ+Ag5/H0jH85nVEdfbOu3ZsScH24HPNmI0OYYXrvnNgBFXkFsRQlQezljV2NSz9TZ3KoU60g4TE7DZqqDZ3fSYC1nLyBwCC7E4VKaWBBE1CACGvnd4GZW/gXcy+SOc9gkjkcVbe7UYMh1BeutBX7y7V9NObU9DcY5trf041X7vbUk1kd7ztvFIzJ0WiWSGd7hGQTXG4e06V2oEg7wVCGh/tWmftdQJZR4PVIUQo+OJP0wOlzCtS0UQXENJ/dSlGgQ9arBTw8Zt00yt4KJU16HoPx3Vj4wyO2DupNxPSwD5su//eZhiCpfpcv+zP9zKAkymIebI5KPGyiiLR48lGKVYHMmkSd0a2tcPZFhXOfxCK41WOL+XpgfktwXKHCBy5NY0LXqZHg+hqHQeb+UfIoNQxOzcPEIaxPOIWw0Qd2Acz7MdGbWFqf3n+qDE/RlLyJZYvuPW4a2XeFBQ==

On Wed, 20 May 2020 14:57:02 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> >
> > Is it sufficient to leave out the "OA :> Ordered A", and instead
> > define an instance like this?:
> > Instance KOO(A Key : Set)(OK : Ordered K)(KO : KeyOrdered A K OK)
> > : Ordered A.
> > If I add this instance (which is easy to fully define), will every
> > "KeyOrdered A K OK" be considered an "Ordered A"?
>
>
> Yes

Thanks, Jason.

My instincts were telling me that I'd be missing some
capability if I did it this way, probably just because it seems wrong in
the classic object-oriented programming language sense to create a
superclass/subclass relationship by declaring an instance.

-- Jonathan

[Coq-Club] typeclass substructure question, jonikelee AT gmail.com, 05/20/2020
- Re: [Coq-Club] typeclass substructure question, Jason Gross, 05/20/2020
  - Re: [Coq-Club] typeclass substructure question, jonikelee AT gmail.com, 05/20/2020