diff options
author | charguer <arthur@chargueraud.org> | 2018-01-19 08:39:05 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 13:31:09 +0100 |
commit | 1274261b6ac020468ac6f24d68de723ae1259c42 (patch) | |
tree | d16180a6e649b9e0cf2b8e74f56e9f33e2de1fec /test-suite | |
parent | 22bf4efd61b916abc81e41bbe70428e534dd0013 (diff) |
added test for coercion from type
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/coercions.v | 34 |
1 files changed, 32 insertions, 2 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index d4fa132d1..9389c9d32 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -130,7 +130,7 @@ Local Coercion l2v2 : list >-> vect. of coercions *) Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). -Section what_we_could_do. +End what_we_could_do. (** Unit test for Prop as source class *) @@ -155,4 +155,34 @@ Module TestPropAsSourceCoercion. (* Print test. -- reveals [hpure] coercions *) -End TestPropAsSourceCoercion.
\ No newline at end of file +End TestPropAsSourceCoercion. + + +(** Unit test for Type as source class *) + +Module TestTypeAsSourceCoercion. + + Require Import Coq.Setoids.Setoid. + + Record setoid := { A : Type ; R : relation A ; eqv : Equivalence R }. + + Definition default_setoid (T : Type) : setoid + := {| A := T ; R := eq ; eqv := _ |}. + + Coercion default_setoid : Sortclass >-> setoid. + + Definition foo := Type : setoid. + + Inductive type := U | Nat. + Inductive term : type -> Type := + | ty (_ : Type) : term U + | nv (_ : nat) : term Nat. + + Coercion ty : Sortclass >-> term. + + Definition ty1 := Type : term _. + Definition ty2 := Prop : term _. + Definition ty3 := Set : term _. + Definition ty4 := (Type : Type) : term _. + +End TestTypeAsSourceCoercion. |