coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat
- Date: Wed, 6 Sep 2017 09:15:17 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jacques-henri.jourdan AT normalesup.org; spf=Neutral smtp.mailfrom=jacques-henri.jourdan AT normalesup.org; spf=None smtp.helo=postmaster AT ulminfo.fr
- Ironport-phdr: 9a23:lvHkohWvvOpyncO13Z44akMUZirV8LGtZVwlr6E/grcLSJyIuqrYZhSEt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aNwvyLzV1J/j4X8v7x4Tyjrjqus6bXwIdjz2kJLh2MR+erAPLt8BQj5ExBLw2z07rq3BRZulNgENlI0iS1zT7+9289ZgrpyZZsOs8+tUFUaj8ZaV+T7tFFjgvNUgz49fuvB3OVhaXoHwGXTNFwVJzHwHZ4USiDd/KuSzgu784gXHCMA==
Hi,
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.
--
JH
Le 06/09/2017 à 07:49, Guillaume Melquiond a écrit :
> On 06/09/2017 01:14, Jan-Oliver Kaiser wrote:
>> Hey everyone,
>>
>> List.tl and List.repeat are outliers in the List module as they
>> introduce new universes which upper-bound list's own universe variable
>> in the global graph. Why is that?
> Good catch. They are created because of the implicit argument of nil,
> which is of type Type. I have no idea whether this deficiency of Coq is
> easily fixed, but we can at least remove these superfluous universes by
> explicit setting the argument of nil in the definitions of tl and repeat.
>
> Best regards,
>
> Guillaume
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jan-Oliver Kaiser, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Matthieu Sozeau, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jan-Oliver Kaiser, 09/11/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Matthieu Sozeau, 09/12/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
Archive powered by MHonArc 2.6.18.