Version française
Home     About     Download     Resources     Contact us    
Browse thread
GADT constructor syntax
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Lukasz Stafiniak <lukstafi@g...>
Subject: Re: [Caml-list] GADT constructor syntax
On Sun, Dec 5, 2010 at 9:10 AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
>
> I don't think that it is very different. Standard-language constraints
> are outside of implications, so they apply to each branch. It already
> behaves this way in the standard language, basically restricting the
> type family to "int term". So I don't see why
>
>> | Embed of 'a : 'a term
>>   constraint 'a = int
>
> shouldn't mean that Embed is "basically" Embed of int : int term.

[To clarify: and the whole family restricted to "int term".]