diff options
| author | Kenji Maillard | 2020-04-22 17:05:44 +0200 |
|---|---|---|
| committer | Kenji Maillard | 2020-04-22 17:05:44 +0200 |
| commit | 6803af12007d388f7bf1fe5f181ea3b6404721b5 (patch) | |
| tree | ab7eb3b47efbee8cd473b95c0f1704bde6354ede /doc | |
| parent | 0c4775fcb48207c96752b81c76f67c17e5fd3c99 (diff) | |
Document `+` in polymorphic universe levels
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index a08495badd..2958d866ac 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -227,7 +227,7 @@ constraints by prefixing the level names with symbols. Because inductive subtypings are only produced by comparing inductives to themselves with universes changed, they amount to variance information: each universe is either invariant, covariant or -irrelevant (there are no contravariant subtypings in Coq), +irrelevant (there are no contravariant subtypings in |Coq|), respectively represented by the symbols `=`, `+` and `*`. Here we see that :g:`list` binds an irrelevant universe, so any two @@ -426,6 +426,19 @@ mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one can use :cmd:`Show Universes` to display the current context of universes. +It is possible to provide only some universe levels and let |Coq| infer the others +by adding a :g:`+` in the list of bound universe levels: + +.. coqtop:: all + + Fail Definition foobar@{u} : Type@{u} := Type. + Definition foobar@{u +} : Type@{u} := Type. + Set Printing Universes. + Print foobar. + +This can be used to find which universes need to be explicitly bound in a given +definition. + Definitions can also be instantiated explicitly, giving their full instance: |