coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strange subtyping

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Strange subtyping
Date: Thu, 7 Jun 2018 17:35:44 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 6.mo178.mail-out.ovh.net
Autocrypt: addr=mail AT maximedenes.fr; prefer-encrypt=mutual; keydata= xsFNBFRYkvgBEAC0Zot4S5lKkhzYK68sSb69wVyEsugASVeWPHjVpxgFG44BLFB7Te0zWHjg jK76yCUmDdpKFdIufw5PQr+3At/8G75Y3x+dGC2rg+31fPAUJvp/AfrMloH+qd+tqxbaKjtC kymLGE01Yj8m3xaV7bN9wuYwL03+staTESJFVm3CZwNAqFgIZCG6KgBGT93ybUgbPYRrTv+n Oleags7nHdPubX6SAWbZVhuweHCwiooRBVSjzyxuhTtDuAwmeZ+ca4WE3IkOWmJmq4KbCeij HJ9B2b6qSopM19dq+iBByPu+LpBCwSA9Nr9hL1XRnoNngwf0OtJ0CNiKjKsNKlAmsCHw/o48 0IoiKP40sH+zsNFeNepbIqILPaWDvTOFvtHc9FDcH2X9NHaWx73GckMzi2z5Ty4tVoEU4Tap JlDVaKWyhvtHRwxbekgk3Vq3PcKKhcLy/xsbyknVLFw8UbFj+sYwGPrzb7j2WhpisfSct3Ii vxv2FUzM3etqM+tsJ/1Oq8u1A5lQ7lSEZmsCQdeyzMXmrUgXAEZvcx5anmTlNR3TjoG6sOxm axp9f/zgZmr9pV/FRq9tLIu8Eqv8+HqeUcHfxICcnXHVPz2x1h6H6ft45h9LGPEi1riCiZZ5 eFnq/epTkpQF411fo7sY1osaZ0Sp9yrHIPAtmJT40tmPQflSYQARAQABzSZNYXhpbWUgRMOp bsOocyA8bWF4aW1lLmRlbmVzQGlucmlhLmZyPsLBdwQTAQoAIQUCVFiS+AIbAwULCQgHAwUV CgkICwUWAgMBAAIeAQIXgAAKCRAWr2+lkXvTQPz8D/4lUpXfqOp0ZVc9WTBr8bDxHE334Bd9 FnekcYCRrmOUE76oMsK1/MhoKCEmr5bdyn8oh/r2GsNTWB1lsHpTEjYc2Sf17LNW2ncVu4OB EsD38chB9aTEev5Pc2jAA7l/WF8ceF5mkt6OjWrBfDp6yBfXwrzDfdzLixVHVyJUYA/04T7U JZc7Rjz1CdXE2wg8KL7+uq/QGc5TCPPQmlpdXJYpDgK7FtJasRoh34/pVFGHXXA1PnCe+IIL 52DynkF+bCL3sWk8A71ebUkyTO6ytqUKYafCPjrrGv4y13O+/2QcB3Iz4gDiKgvL8FWMhmhJ QF5C8BucOE87JWb5nJmq+Gs13NVofYMpmI+DDaBNJ6ns/sbR68vRfoXEhr0adPDLZOohZKJM Lu6WTjyFNNOgj1jgG0I00+tctmtW00W+U3oi36vbUXalbi5WPlIBpIXkjI9p7xoHe1mJwN40 jn/ExEXnY9uZ4H/NorJ7OzGdEOlz+ZpkcBpW34N5GZfOg7UXScA3tAFPyWcxCKsxAti0sRAR fIQXkxwt+BTBMm5m7n+wxe/2sf+xxO6AYyedWRbLaTCexJEw4Tx4+hocFT8lD6y/cGPORcak AkoWz2aiGQK07gbJ5dxymCP6g0Xcl8CloXodwV124G2++eQpucydK4BRFDTyJLJJNAR3nkei s1BBj87BTQRUWJL4ARAAqLecjPrMCx42r822nQT6e8GTHrFKwppkRqSXAucAZ4ICJ1YoT2Hy z+DtehqEV5IdIDGRivKvQYQF1Yz2NpgO7vfmB1M8ZsxyTyFeQiBkFIb5BKVhUk0xat2Xjgmb PJ59GsEbH5DCIrUqFRRGshjgul/z0adUF5DjFyuqo5TMAJdgXtJbTzmCTXoBwJmNuaUHwieK s47K9pmnnaUnkSy+CDTjtOihNeSx+lmrzieo8OyYuwvY1V1av+dJlF6YF7D5X9gHUAMsSypq pdQX0PhUZ4XheCiC0HojVzT3NEEkZ3LjuAGD7+1yaWNepGgqFqiaGEq4ihjihbvW3rCO84RS 9rSb6F7Eru7HMDUKLmUDc37GhOC0xcrTJ5zZ0CwTaM6V2P2n/FxOXEoKwRVGdAAWvh521N7k pYQpGsamfCzl8ruaEf/IhksPZiyJC95W5jXl98UDf6WNm/xKXwF60oK56iSBj+YWmUgjAzGf XRCJyiXAlMtBhErkije2iIqKVungP3N4IPEhmDOLVa9BsdXAsptkWSmWzvJA+z0A52hta0/2 B71dreoGFVnmLWWSCR+O6P9yivnfEKq75QPjBLj6xw6nXxtyhyrVT2/xOy1Osvf2mM7Gx9wR Q0Ktv7fjX2AyIrcvR3r3/RgsDA3/elqkcrY1hdu+NkOHOKtME43htXsAEQEAAcLBXwQYAQoA CQUCVFiS+AIbDAAKCRAWr2+lkXvTQNfiD/0fD2LeHa/7Vq7ClzMgjaCm5Jt2afGZi9xrD+Z8 4/wlVjFI8TZsYoiq6OTbvn6eNFE7J0wYpAouYS6GP/Ga+e/eo9Hm3BeK9+1gP0QSfwcA1+ci n+zvD5q58Movy7qo4BOoJM2eb8FpdyeloViTUlxgqocZK35ewTK0q3JcMlSZZxdOvCol3F8r CWkXqHlJoA9dL16VxBbxmT57ogqgpOFfIbc9PHMjQaNY5BWLz1+qj4bXN5UXvibP97tas1LE 4OilGPIW/ZOMItfVcxi9//huyTJt0l4lRJRochpmppItYeDs6tFyFu4XpEgUbAXwTnANqHr2 N0OSZT3j+BTMgVrs5sUgjMlqNJkMKjZmkIuSoIZbtYHfQgSY2VBPImLyWpu+XdzjBwFbuMJK 8q9tvgG2ydZCDbpC6Bi0FF+WKmZZqSkqgIFjUOkLGh624JQLbU/aezYrrhORDGEIAGtHbdn3 pC1fcAJHwI3JpRpNwou+lc8SORjUoTpSOmc5C0qWu0P7D1Y3k8gFngN/c42TX6eyyVpQw44h A6bxBs56DrE8OPyt15lveeMxT/0scd/MJlFJY/Dy+XelA0Utt0SUgSqI+TaL2eTlwNCmhNL+ ShCTVRcfb1UFlSA+GyURCLoUjrbukm7GS0pKhF+O9eCj1DkYEdi9NTjs83wKHHYu8CspWw==
Ironport-phdr: 9a23:C0cdAR9DuwOYgv9uRHKM819IXTAuvvDOBiVQ1KB40egcTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LWbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUIFeUAMudYr4zjqFAToxW5Hw+sA/r0yjRVgXL22Lc10+UlEQzd2QwvBd0PsHXRrNrrKagdT+a1w7fTzTnZYfNWwy7w5Y7VeR4iufGBRb19fMvLxUUyCw/Ijk+cpIzrMj+Py+gAvXaX4/J9We+hiGMrsQV8rzm1yssyloXFmpgZxk3H+Ch/3Y07P8e3SFRhbt6hCJZQtz+VN49xQs46QmxkoiM6yrobtZO5fyUG0pEnyATea/yDaoSI5Q/jVPqLLTd/mnJleKizhxCs/ki80uH8V8+030hWriddndTBt2oB2wHP5sWHUPdw/kms1SyS2w3d9O1IOUU0mrDaK54lzL4wjJ0TsUHbEy/zgkr2jauWe14h+uey5OXnY7DmqYGBOIBqjAHxLL8ultaxAeQiKgQORXSU+fyg1L3/+k30WKlFjvovkqXArJ/aIdkbqbWiDg9O0ocj7g6/AC283NQZm3kHNlNFdwidg4jnIVGdaMz/WPy4mhGnlCph7/HAJLzoRJvXfVbZl7K0WL9t6ktRgCayy1BEr8ZRA7AFCPf6Sk70udDVCBIidQKulbW0QO5h358TDDrcSpSSN7nf5AfRt7AfZtKUbYpQgw7Tbv0s5vrgl3g8wAFPeKC53J4aZH2+E+8gLV/LOCOw0OdEKn8Du08FdMKvkEeLCGABYn+iXqcx6jw9BZngA52RHtnw0ozE5z+yG9htXk4DCl2IFi22JdvCXvBVN3LUJ8ZglnkDSKTnTJEhkxejqF2ixg==
Openpgp: preference=signencrypt

For that, no need to have it in the theory or the kernel. We could have
a notation `Set := Type` (if they play exactly the same role).

Maxime.

On 06/07/2018 05:33 PM, Stefan Monnier wrote:
>> I'm not sure why we would keep Set in your proposal, though. Does it
>> play any role?
>
> Support the many lines of existing Coq code which mention Set?
>
>
> Stefan
>

[Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
- Re: [Coq-Club] Strange subtyping, Matthieu Sozeau, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
    - Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
      - Re: [Coq-Club] Strange subtyping, Stefan Monnier, 06/07/2018
        
        Re: [Coq-Club] Strange subtyping, Maxime Dénès, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/07/2018
  - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/09/2018
    - Re: [Coq-Club] Strange subtyping, Théo Zimmermann, 06/09/2018
      - Re: [Coq-Club] Strange subtyping, Helmut Brandl, 06/15/2018