Subject: Ssreflect Users Discussion List
List archive
- From: Arthur Azevedo de Amorim <>
- To: "" <>
- Subject: [ssreflect] Phantom types and "*_of" aliases
- Date: Wed, 06 Dec 2017 21:59:11 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
- Ironport-phdr: 9a23:nf11gByrGFqGEwTXCy+O+j09IxM/srCxBDY+r6Qd0esXIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSj49iUIFxv7OAFpDuHuAMvTid623qaz/YfSakNGnnD1NahpNhi4qQjaquETmpEnK6AryxKPo31Seu0Qy3k+dnyJmBOpz92s/IN5uw1Ctuws+8kIXaiyVqE/V71dRGAvKXw1+detvBDrQg6G539aWWITxEkbSzPZ5Q33C8+i+hDxsfBwjXGX
Phantom types are used in several places of mathcomp to infer canonical structures. Is there any reason for preferring, e.g.
Record my_type (T : eqType) := MyType {value : T; _ : some_pred value}.
Definition my_type_of (T : eqType) of phant T := my_type T.
over
Record my_type (T : eqType) (p : phant T) := MyType (value : T; _ : some_pred value).
?
- [ssreflect] Phantom types and "*_of" aliases, Arthur Azevedo de Amorim, 12/06/2017
- Re: [ssreflect] Phantom types and "*_of" aliases, Enrico Tassi, 12/07/2017
Archive powered by MHonArc 2.6.18.