The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

My naive understanding is that it would create a fresh (set of) universe
variable, and copy all the edges of the existing universe variable of
the list inductive type. But there should not be any direct constraint
between the fresh universe to the one of the original list definition.

-- 
JH

Le 06/09/2017 à 10:14, Guillaume Melquiond a écrit :
> On 06/09/2017 09:15, Jacques-Henri Jourdan wrote:
>
>> What's strange, to my point of view, is that list is template universe
>> polymorphic. My interpretation is that it does mean that any use of list
>> (and of nil) after its definition should not create new constraints of
>> list's own universe variable, but rather create a fresh universe
>> variable and add constraints on this variable.
> I don't understand your point. Once it has created a fresh universe
> variable, any meaningful constraint on it necessarily involves the
> universes in the definition of list. How else would you constrain this
> fresh universe if you cannot relate it to an existing one?
>
> Best regards,
>
> Guillaume

Attachment: signature.asc
Description: OpenPGP digital signature