coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat
- Date: Wed, 6 Sep 2017 10:14:02 +0200
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
- [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/13/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.