coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Mysterious Universes introduced by List.tl and List.repeat

From: Jan-Oliver Kaiser <janno AT mpi-sws.org>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat
Date: Wed, 6 Sep 2017 01:14:53 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=janno AT mpi-sws.org; spf=Pass smtp.mailfrom=janno AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:qYI5JxDawR9bmW9r7q3yUyQJP3N1i/DPJgcQr6AfoPdwSP3zp8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHUB74LE9+Ivn/Mo/UlcW+ke6osdWHaAJRwTG5fLlaLROsrAyXuNNA0qV4LaNk6BLP51xMevpb3ytLLFOIkgy0ssW5+phk2yFIurc66NUGVr/1KfdrBYdEBSgrZjhmrPbgsgPOGFOC

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?

What confuses me is that these universes do not show up in the actual definition.

Thanks
Janno

P.S.: in case it matters:
$ coqtop -v
The Coq Proof Assistant, version 8.6.1 (August 2017)
compiled on Aug 8 2017 15:55:58 with OCaml 4.02.3

[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