diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/5692.v | 54 |
1 files changed, 52 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v index 55ef7abe4..4c8d464f1 100644 --- a/test-suite/bugs/closed/5692.v +++ b/test-suite/bugs/closed/5692.v @@ -1,9 +1,59 @@ Set Primitive Projections. Require Import ZArith ssreflect. -Module Test3. +Module Test1. -Set Primitive Projections. +Structure semigroup := SemiGroup { + sg_car :> Type; + sg_op : sg_car -> sg_car -> sg_car; +}. + +Structure monoid := Monoid { + monoid_car :> Type; + monoid_op : monoid_car -> monoid_car -> monoid_car; + monoid_unit : monoid_car; +}. + +Coercion monoid_sg (X : monoid) : semigroup := + SemiGroup (monoid_car X) (monoid_op X). +Canonical Structure monoid_sg. + +Parameter X : monoid. +Parameter x y : X. + +Check (sg_op _ x y). + +End Test1. + +Module Test2. + +Structure semigroup := SemiGroup { + sg_car :> Type; + sg_op : sg_car -> sg_car -> sg_car; +}. + +Structure monoid := Monoid { + monoid_car :> Type; + monoid_op : monoid_car -> monoid_car -> monoid_car; + monoid_unit : monoid_car; + monoid_left_id x : monoid_op monoid_unit x = x; +}. + +Coercion monoid_sg (X : monoid) : semigroup := + SemiGroup (monoid_car X) (monoid_op X). +Canonical Structure monoid_sg. + +Canonical Structure nat_sg := SemiGroup nat plus. +Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n. + +Lemma foo (x : nat) : 0 + x = x. +Proof. +apply monoid_left_id. +Qed. + +End Test2. + +Module Test3. Structure semigroup := SemiGroup { sg_car :> Type; |