diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2017-07-27 14:54:41 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
commit | f72a67569ec8cb9160d161699302b67919da5686 (patch) | |
tree | a86642e048c3ac571829e6b1eb6f3d53a34d3db0 /test-suite/success/polymorphism.v | |
parent | fc587e75d2d5d6e67365a9bc3a13ba5c86aba87b (diff) |
Allow declaring universe constraints at definition level.
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
Diffstat (limited to 'test-suite/success/polymorphism.v')
-rw-r--r-- | test-suite/success/polymorphism.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index ecc988507..0bd8bfe60 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -156,6 +156,38 @@ Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d. End structures. + +Module binders. + + Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}. + exact A. + Defined. + + Definition nomoreu@{i j | i < j} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). + exact A. + Fail Defined. + Abort. + + Polymorphic Definition moreu@{i j +} (A : Type@{i}) : Type@{j}. + pose(foo:=Type). + exact A. + Defined. + + Check moreu@{_ _ _ _}. + + Fail Definition morec@{i j| } (A : Type@{i}) : Type@{j} := A. + + (* By default constraints are extensible *) + Definition morec@{i j} (A : Type@{i}) : Type@{j} := A. + + (* FIXME: not handled in proofs correctly yet *) + Lemma bar@{i j | } : Type@{i}. + exact Type@{j}. + Defined. + +End binders. + Section cats. Local Set Universe Polymorphism. Require Import Utf8. |