aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2928.v
blob: 21e92ae20ca8bec603aa485dec4914ca264a25c1 (plain)
1
2
3
4
5
6
7
8
9
10
11
Class Equiv A := equiv: A -> A -> Prop.
Infix "=" := equiv : type_scope.

Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.

Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.

Class SemiLattice A op `{Equiv A} :=
    { semilattice_sg :>> SemiGroup A op
    ; redundant : Associative op
    }.