From 0bba5da999dc8eeef75c7040562f687ce589ed11 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 14:04:34 -0400 Subject: Add test-suite checks for coqchk with constraints --- test-suite/coqchk/univ.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'test-suite/coqchk') diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index 84a4009d7..19eea94b1 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -33,3 +33,16 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) := (rank_injective : injective_in T natural D rank) (rank_onto : forall i, equivalent (less_than i n) (in_image T natural D rank i)). + +(* Constraints *) +Universes i j. +Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})). +Constraint i < j. +Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}). +Universes i' j'. +Constraint i' = j'. +Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})). +Inductive constraint4 : (Type -> Type) -> Type + := mk_constraint4 : let U1 := Type in + let U2 := Type in + constraint4 (fun x : U1 => (x : U2)). -- cgit v1.2.3