coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] universe polymorphism flag when loading file

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] universe polymorphism flag when loading file
Date: Wed, 8 Jan 2020 08:55:39 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=S1xjZVzyjwEqp8dWaAdOleBXA3f+jSDZKdrYcu4P5Ic=; b=iBIhGn2Y597xv1D06ENJi6IZkQ4lO3AuuzmeTVXJRXikt8gzcIYM39/SHAtZ9hksQJ/A1ESjjZkOj0HcZnYekzhLQLjhPyE0OrxLd8AmJ59vk4X/2CMSsyQ2cLLLL+vq1c+m5AfC2Xuii9cDDq5PdNxccMpgOqZJqC99KZGxoyO6T1Ep4fghXNPJfS/XeJtIxAF4IsXGVSv11nzn/Dm1tVRFhi9JaiET/5tzkV+Z7GTyA9UmVEVpOpKnLmD1PvB8QJCRhEushaKqg84CyMg5UBSS/xSjd07PXF0q2VDoL9A5TTd0yY2mr8hDuc5YuXaoMG0GsD+vX6vfwGD0dnDPrA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=RGso+Tpv56PhM3nDJldD72JGuDoFdZlgolTHGOxB5bIkg0FWBww8NOYNRcRv1NaQlgwD435Pe8UyYe+N9IEX578zx6TTL+TjA6+26IjLy2kFyo1nr8KYJ5iD/kw0TPCEEp8GBjSju9xH2dEl/teCHJbvQ67FPEnl4NAqm8h3U180vwZYQ5cIjxb+Wd8pBFpxEihuCA9rpJi38VKXPAsloyMu31cv/psWeB3AUTrmzkNeDNcM3oNqhq2e0JxI1mIYfeBYZN9Nev+Re2zLYgiqkkzYx9NryN06PtXPVgIJUODOG0JCLD/NKAeC3SZiPhc3+Xt+WEQ4f0u+mntxj91Irg==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:onnSBBMxnA5PJ1rQc3sl6mtUPXoX/o7sNwtQ0KIMzox0Iv7yrarrMEGX3/hxlliBBdydt6sfzbCL7Ou5AzBIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfL1/IA+ooQjRtMQajpZuJrg+xxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKjg0+3zVhMNtlqJWuBKvqQJizY7Ibo+bN/t+cb/Sc9wVXmdBQt1eWjZdDo+gc4cCDewMNvtYoYnnoFsOqAOzCw2yC+P11DBIg3/31rA03es7HwDGxwsgH9QTu3nTqNv6Kr0SXv6wzKjI1znNYelZ2Dnm6IjPdBAsuuuDXbRtccbL10YgCh7Fgk+Kpoz4Jj6Y0PkGvWuD7+d4Wu+jl3QrpxxtrjWt3Msgl4fEi4MPxlzZ+yh0w545KNK8RUJhfNKpFJtduzuHO4Z4Qc4uWWNltSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wr/WemfPDl0mG9pdKu4iRi97ESs0+r8WdKq31pQqSpFj8XMuWsK1xzO7MiIV+Fx/l+72TaIywDc9P1LIVw1larcLZ4t2LkwlocPsUTHGS/2n0b2gLWKeUUj/+ik8+XnYrP4qZ+AL4J5hR3yPr4zlsCjA+k0KBUCUmaa9OimybHu8070TK1PjvIsk6nZtJ7aJd4cpq68GwJb1pgs6wyhADej0NUUh3cJI0hLeRKciIjpPUrDL+r+DfeimVijjipkx+3cMrL7H5XBNmLDn6v5fbZh905czxI+wsxY55JNE70OPPbzWlLqu9HDFR84Mwm0w/79B9ln14MeX3iPAq6DP6/Iv1+I/LFnH+7ZLoQSoXP2L+Uvz//ol34w31EHN+H91pwOLXu8A/5OIkODYHOqjM1XQkkQuQ9rbuHwhViTGRJaeG21WepoxDwhBYe3S6vKWZuqhpSI2jr9E5FLIGlbXAPfWUz0fpmJDq9fIBmZJdVsx2RdCOqRDrQ53BTrjzfUjrpqKu2IpX8xiKm7jZ1QyrSWkhs/sztpE86azmeBCXlumX8FTCM326Y5plFhzlCE0u5zhPkKTIUCtcMMaR8zMNvn98I/DtnzXgzbedLQEgSvRMjgDD0sCNsskYZXPxRNXu66hxWG5BKERqcPnuXRVpUy7+TR02W3Ltsvk3s=

Hi,

I don't understand this behaviour

Given a file sup.v as follows:

Set Universe Polymorphism.
Test Universe Polymorphism.
Set Printing Universes.
Test Printing Universes.
Definition relationT (A : Type) := A -> A -> Type.
About relationT.
Test Universe Polymorphism.
Test Printing Universes.
Print relationT.

when I load the file the flag Universe Polymorphism doesn't apply to the
definition of relationT, and gets turned off (though another flag I
tried doesn't get turned off)

[jeremy@localhost modal]$ coqtop -color no
Welcome to Coq 8.8.2 (January 2019)

Coq < Load sup.
The universe polymorphism mode is on
The printing of universes mode is on
relationT is defined
relationT : Type@{Top.1} -> Type@{max(Top.1,Top.2+1)}

Argument scope is [type_scope]
relationT is transparent
Expands to: Constant Top.relationT
The universe polymorphism mode is off
The printing of universes mode is on
relationT =
fun A : Type@{Top.1} => A -> A -> Type@{Top.2}
: Type@{Top.1} -> Type@{max(Top.1,Top.2+1)}
(* {Top.2 Top.1} |= *)

Argument scope is [type_scope]

whereas when I compile the file I get (as I would have expected)

[jeremy@localhost modal]$ coqc sup.v
The universe polymorphism mode is on
The printing of universes mode is on
relationT@{sup.1 sup.2} :
Type@{sup.1} -> Type@{max(sup.1,sup.2+1)}
(* sup.1 sup.2 |= *)

relationT is universe polymorphic
Argument scope is [type_scope]
relationT is transparent
Expands to: Constant sup.relationT
The universe polymorphism mode is on
The printing of universes mode is on
relationT@{sup.1 sup.2} =
fun A : Type@{sup.1} => A -> A -> Type@{sup.2}
: Type@{sup.1} -> Type@{max(sup.1,sup.2+1)}
(* sup.1 sup.2 |= *)

relationT is universe polymorphic
Argument scope is [type_scope]

What is happening here?

Thanks

Jeremy

[Coq-Club] universe polymorphism flag when loading file, Jeremy Dawson, 01/08/2020
- Re: [Coq-Club] universe polymorphism flag when loading file, Gaëtan Gilbert, 01/08/2020