Subject: Ssreflect Users Discussion List
List archive
- From: Bas Spitters <>
- To: Ssreflect-mailinglist <>
- Subject: [ssreflect] eqType for records ?
- Date: Mon, 18 Jun 2018 17:37:45 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
- Ironport-phdr: 9a23:FKgChh9+Fhyrgf9uRHKM819IXTAuvvDOBiVQ1KB30eMcTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RPXchfSjJPDZ+nYosTE+YMJ/pUo5Xhq1YMqxa1GAmiBPnoyj9NnnL7wLc10/88Gg/bxAwgHs4OsGjKo9XvL6cZTOe4w7LSwTrZdf9X1y3x6JPQchAgvfGMQax/cdDKyUQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyhWAnrARxrSKuxscqkoTJiYMVykzE9SVk24k5P8G3SEl+YdOiDZBetDmaOpNoTs8+R2xkoiU3x70ctZKmfSUG1Y4rywPdZvGGdYWD/wjtW/yLIThigXJoYLK/iAi28Uin0uD8U9O70FdOriZcktjNuGwB2wXd6sSaSPZw/12t2TmI1wDU5eFEJV47mbDHJJ4mx748jpsTsULdES/qgEj6krOae0E+9uWr6+nreKjqq56BO4Nulw3zMKUjltS6AesiMwgOW2ab+f671L3m5UD2W69GgecsnqjXqpzaPtwbpq+lAw9JzIkj8Q2/Aiyp0NQdh3YHLVZFdAibgIjuPlHCOOr4Auung1SwjDdrwOjLPqb6ApXXMHfDnrPhcqhh5E5A0wcz1tBe55dMCr4bOv7zW0nxtMbZDhAjKQC0zfznW51B0dYlQniCDKuUO7+XtFaJ4uMpLO2Nf5Nd7C3mMfUr4/PlkVc8gkVYfK+z3JJRaXaiH/0gLV/PMlT2hdJUO24R9jEmTfD2hUeZGWpZIX/0QOQn/jAnFI+8Fq/MQ4mshPqK2yLtTc4eXXxPFl3ZSSSgTI6DQfpZLXvKepYwwAxBbqCoTsoa7T/rsQb7z7R9Ke+No38XsJvi0J5+4OiBzEhupwwxNNyU1iS2d08xhnkBHmZk06V2oEg7wVCGg/Ah3q5oUOdL7vYMaT8UcJ7Ry+sgVYL3UwPFO8aWEBOoG4r4Rz42Sd01zpkFZEMvQ9g=
Is there an established way to obtain an eqType on a Record?
I'd imagine first proving that eqTypes are closed under Sigma-types
and then converting records to Sigma-types, as e.g. is done in the
HoTT library:
https://github.com/HoTT/HoTT/blob/master/theories/Types/Record.v
Thanks,
Bas
- [ssreflect] eqType for records ?, Bas Spitters, 06/18/2018
- Re: [ssreflect] eqType for records ?, Emilio Jesús Gallego Arias, 06/18/2018
- Re: [ssreflect] eqType for records ?, Christian Doczkal, 06/19/2018
- Re: [ssreflect] eqType for records ?, Emilio Jesús Gallego Arias, 06/19/2018
- Re: [ssreflect] eqType for records ?, Emilio Jesús Gallego Arias, 06/19/2018
- Re: [ssreflect] eqType for records ?, Cyril, 06/19/2018
- Re: [ssreflect] eqType for records ?, Emilio Jesús Gallego Arias, 06/20/2018
- Re: [ssreflect] eqType for records ?, Cyril, 06/19/2018
Archive powered by MHonArc 2.6.18.