diff options
author | Amin Timany <amintimany@gmail.com> | 2017-05-02 19:53:05 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:17 +0200 |
commit | d6898781f9cd52ac36a4891d7b169ddab7b8af50 (patch) | |
tree | 880ef0bcad043f083a6157644d10e068b8185b4c /test-suite/coqchk | |
parent | 4bf85270a36a0a3f9517d8bce92d843f882af00a (diff) |
Correct coqchk reduction
Diffstat (limited to 'test-suite/coqchk')
-rw-r--r-- | test-suite/coqchk/cumulativity.v | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v new file mode 100644 index 000000000..5d245aaa5 --- /dev/null +++ b/test-suite/coqchk/cumulativity.v @@ -0,0 +1,52 @@ +Set Universe Polymorphism. +Set Ind Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. +Proof. reflexivity. Qed. + +Inductive Tp := tp : Type -> Tp. + +Section TpLift. + Universe i j. + + Constraint i < j. + + Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. + +End TpLift. + +Lemma LiftC_Lem (t : Tp) : LiftTp t = t. +Proof. reflexivity. Qed. + +Section TpLower. + Universe i j. + + Constraint i < j. + + Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. + +End TpLower.
\ No newline at end of file |