Subject: Ssreflect Users Discussion List
List archive
- From: Arthur Azevedo de Amorim <>
- To: Maxime Dénès <>,
- Subject: Re: [ssreflect] Empty type
- Date: Thu, 12 Oct 2017 12:54:36 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
- Ironport-phdr: 9a23:P60vVxAmZpTIGVNuU3exUyQJP3N1i/DPJgcQr6AfoPdwSP76o8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHPxzvNA94bsh0HA7Jx5Cy3uG205jacwRNiTawZ75pahus+0GZrdIMjIVmJ60t4h7SuD5Jff5XzCVpI0iSllDy/JSe5plmpg1Kp/I87YZpQ6jkcqg/BbBVRB0jNHo04YW/vAPfTRaVoHIVemoTmxtMRQPC6UepDd/KriLmu78li2GhNsrsQOVsVA==
Hi Arthur,
That's an interesting observation. Just curious, what use cases do you
have in mind?
Maxime.
I want to build a recursive type as the fixed point of a functor by taking the union of the F^i(void).
It is true that it would be possible to use 'I_0 instead, but I feel that void is special enough to deserve a separate type.
Arthur
On 10/12/2017 12:11 AM, Arthur Azevedo de Amorim wrote:
> I was hoping to find instances of the basic ssreflect classes for
> Empty_set or some other empty type, and to my surprise there aren't
> any. (The eqtype library still says: "The eqType interface is
> implemented for most standard datatypes: bool, unit, void, ...".)
>
> Do others think it would be useful to include that in a future release?
>
> Arthur
- [ssreflect] Empty type, Arthur Azevedo de Amorim, 10/12/2017
- Re: [ssreflect] Empty type, Maxime Dénès, 10/12/2017
- Re: [ssreflect] Empty type, Christian Doczkal, 10/12/2017
- Re: [ssreflect] Empty type, Pierre-Yves Strub, 10/12/2017
- Re: [ssreflect] Empty type, Arthur Azevedo de Amorim, 10/12/2017
- Re: [ssreflect] Empty type, Christian Doczkal, 10/12/2017
- Re: [ssreflect] Empty type, Maxime Dénès, 10/12/2017
Archive powered by MHonArc 2.6.18.