Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] eqType for records ?

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] eqType for records ?


Chronological Thread 
  • From: Emilio Jesús Gallego Arias <>
  • To: Christian Doczkal <>
  • Cc:
  • Subject: Re: [ssreflect] eqType for records ?
  • Date: Tue, 19 Jun 2018 09:36:29 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=Pass
  • Ironport-phdr: 9a23:/y087h+J9G50mP9uRHKM819IXTAuvvDOBiVQ1KB41escTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsaS2RfQ8hRUCJBDI2+YIUMAeUOMvpXopLhp1cStxayGRWgCfntxzJOm3T43bc60+MkEQze0wIgGtMOsHDVrNXyLKgcVf66zLLS1TXYd/xY2C3y6IzMch8/rvGMWqp/fNbLyUkuDQzFlUibpIv7MD6O2eUAsHSX4/BnVeK1hG4qsgd8qSWsyMc0koTFm4EYx1Pe+Sln3oo4JMe0RFN5bNK5Cpdcqi+XO5VuTs4iX21kojg2xqEbtZKhciUHyo4ryhrQZvGBboOG+AjsVPyLLjd9nH9leKywhxK18UW4xezxVdW43ExNripfndnArnEN1xrN5cibUvZx40Ss1DWV2wzN9O1JIFo4mbfZJpI82LI8i5QevVrbEi/zgkr2jauWdks++uiv7uTqeqvpq4STNoJ3lg3yKKMumtawAeggKAgBQ3Cb+fig1L3k5UD5W65KjuconanXtJDVO9gUprKiDg9O0ocj7g6/AC283NQZm3kHNlNFdwidg4jnIVGdaMz/WNy/mVW3jDZiwbjqObbzAZzJZizIkK3gZqp84kgaxA0439NW47pZDKpEJOP0XAn/roqLIAU+NlmZxufjCdJK9I4Fy3m4LaadNK7dtmih/OMmOKHYaacF6G67LOIqsa29xUQlkEMQKPH6laAcb2q1S7E/ex3AMCjcx+wZGGJPhTIQCenjiVmMSzlWNiSiD/p64Ss0Wtv/UdXzA7u1ibnE5x+VW4VMbzEUGgDUV3DyeNfcAqpeWGepOsZk1wc8e/2hRosmhEO+5Fe8zKBofLPZ
  • Organization: X80 Heavy Industries

Christian Doczkal
<>
writes:

> From that it is not to hard to get an eqType instance also for
> dependent record types (see below). Not sure though how to best
> generalize this over the constructors of a concrete record type or how
> to best iterate this.

A simple hack to implement would be just to extend the [newType ]
notation to different arities, so [newType2 , [newType3, etc... are
introduced.

With a bit more effort a generic arity implementation maybe would be
possible.

E.



Archive powered by MHonArc 2.6.18.

Top of Page