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: Cyril <>
  • Cc: Christian Doczkal <>, , Bas Spitters <>
  • Subject: Re: [ssreflect] eqType for records ?
  • Date: Tue, 19 Jun 2018 22:41:01 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=Pass
  • Ironport-phdr: 9a23:JP8VXR2t/2BYCKXpsmDT+DRfVm0co7zxezQtwd8Zse0SKvad9pjvdHbS+e9qxAeQG9mDtrQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYwhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWpPUNhMWSxGDIOyYYkAAekPMulXs4bwvEcOoQekCAWwGO/i0D1Fi3nr1qM6yeQhFgTG0RQvEdILsXTUqNT1NKAKXu6x0qbI1i/bb+hO1jn88ofIdhQhru+DXbJ3acXc1VMvFwLfgVWLtIfoOC2a2/8CsmWY8+ZsT+Wvi3QoqwxopDWk28QiipHRi44IyV3J9j91zJgrKdC5UkJ3fNypHIZKuy2HOYZ6XNsuTmF0tCog1LEKpYO3cDIExZkl3RLSb/OKfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/XzV8S3zFpGtC1FksPDtnwV1hzT7NaISudl80u82juC1Brf5v9aLU01j6bXNpwszqMqmpYOv0nPADf6mEDsg6+XckUk9PKo6+PiYrj+uJCRLIB1hwLiPqg0ncy/G+s4PhAUX2eH4eS8yKHj/UrhTbVRlf02iLfWsJ7eJcsFuqG5HxRY0p0j6ha6Fzepys4UnXgBLFJfeRKIlZLlO1/UIKOwMfDqqEW2kTMjk/vXJLzlRJ7KLnXFuLbnZ7d0rUBGnlkd19dasr9RC7UAJ8XRV1Rjr+v3Bxs9PgOz9M/9CdxmntcTcXLfWumeKqyE4gzA3f4mP+TZPNxdgz36MfVwoqe21SZoy29YRrGg2N4sUF79G/1nJ0uDZn+90MdRSSENpAVsFbW22m3HaiZaYjOJZ4x5/isyWdC2Xd+FQZqi0uTYgXWLW6ZOb2UDMWiiVHflc4LVCedcMGSVOMAzyzE=
  • Organization: X80 Heavy Industries

Cyril
<>
writes:

> To take the example of Christian, here would be the most canonical way
> to do it.

I would use the (partial) embedding method for types that have more than
one constructor, however for records I still feel that a principle based
on newType may be more economical as it would work for all records of a
given arities.

YMMV of course.

Cheers,
E.



Archive powered by MHonArc 2.6.18.

Top of Page