Module `Verify.Compare`

Provides functors to verify that instances are lawful.

module Medial_Magma : functor (M : Interface.MEDIAL_MAGMA) -> functor (E : Interface.EQ with type t = M.t) -> sig ... end

module Semigroup : functor (S : Interface.SEMIGROUP) -> functor (E : Interface.EQ with type t = S.t) -> sig ... end

module Semigroup_Any : functor (S : Interface.SEMIGROUP_ANY) -> functor (E : Interface.EQ1 with type 'a t = 'a S.t) -> sig ... end

module Monoid : functor (M : Interface.MONOID) -> functor (E : Interface.EQ with type t = M.t) -> sig ... end

module Monoid_Any : functor (M : Interface.MONOID_ANY) -> functor (E : Interface.EQ1 with type 'a t = 'a M.t) -> sig ... end

module Quasigroup : functor (Q : Interface.QUASIGROUP) -> functor (E : Interface.EQ with type t = Q.t) -> sig ... end

module Quasigroup_Any : functor (Q : Interface.QUASIGROUP_ANY) -> functor (E : Interface.EQ1 with type 'a t = 'a Q.t) -> sig ... end

module Medial_Quasigroup : functor (Q : Interface.MEDIAL_QUASIGROUP) -> functor (E : Interface.EQ with type t = Q.t) -> sig ... end

module Loop : functor (L : Interface.LOOP) -> functor (E : Interface.EQ with type t = L.t) -> sig ... end

module Loop_Any : functor (L : Interface.LOOP_ANY) -> functor (E : Interface.EQ1 with type 'a t = 'a L.t) -> sig ... end

module Group : functor (G : Interface.GROUP) -> functor (E : Interface.EQ with type t = G.t) -> sig ... end

module Group_Any : functor (G : Interface.GROUP_ANY) -> functor (E : Interface.EQ1 with type 'a t = 'a G.t) -> sig ... end

module Abelian_Group : functor (A : Interface.ABELIAN_GROUP) -> functor (E : Interface.EQ with type t = A.t) -> sig ... end

module Abelian_Group_Any : functor (A : Interface.ABELIAN_GROUP_ANY) -> functor (E : Interface.EQ1 with type 'a t = 'a A.t) -> sig ... end

module Functor : functor (F : Interface.FUNCTOR) -> functor (E : Interface.EQ1 with type 'a t = 'a F.t) -> sig ... end

module Apply : functor (A : Interface.APPLY) -> functor (E : Interface.EQ1 with type 'a t = 'a A.t) -> sig ... end

module Applicative : functor (A : Interface.APPLICATIVE) -> functor (E : Interface.EQ1 with type 'a t = 'a A.t) -> sig ... end

module Monad : functor (M : Interface.MONAD) -> functor (E : Interface.EQ1 with type 'a t = 'a M.t) -> sig ... end

module Alt : functor (A : Interface.ALT) -> functor (E : Interface.EQ1 with type 'a t = 'a A.t) -> sig ... end

module Plus : functor (P : Interface.PLUS) -> functor (E : Interface.EQ1 with type 'a t = 'a P.t) -> sig ... end

module Alternative : functor (A : Interface.ALTERNATIVE) -> functor (E : Interface.EQ1 with type 'a t = 'a A.t) -> sig ... end

module Semigroupoid : functor (S : Interface.SEMIGROUPOID) -> functor (E : Interface.EQ2 with type ('a, 'b) t = ('a, 'b) S.t) -> sig ... end

module Category : functor (C : Interface.CATEGORY) -> functor (E : Interface.EQ2 with type ('a, 'b) t = ('a, 'b) C.t) -> sig ... end

module Eq : functor (E : Interface.EQ) -> sig ... end

module Quasireflexive_Eq : functor (E : Interface.QUASIREFLEXIVE_EQ) -> sig ... end

module Ord : functor (E : Interface.ORD) -> sig ... end

module Bounded : functor (B : Interface.BOUNDED) -> sig ... end

module Join_Semilattice : functor (J : Interface.JOIN_SEMILATTICE) -> functor (E : Interface.EQ with type t = J.t) -> sig ... end

module Meet_Semilattice : functor (M : Interface.MEET_SEMILATTICE) -> functor (E : Interface.EQ with type t = M.t) -> sig ... end

module Bounded_Join_Semilattice : functor (B : Interface.BOUNDED_JOIN_SEMILATTICE) -> functor (E : Interface.EQ with type t = B.t) -> sig ... end

module Bounded_Meet_Semilattice : functor (B : Interface.BOUNDED_MEET_SEMILATTICE) -> functor (E : Interface.EQ with type t = B.t) -> sig ... end

module Lattice : functor (L : Interface.LATTICE) -> functor (E : Interface.EQ with type t = L.t) -> sig ... end

module Bounded_Lattice : functor (L : Interface.BOUNDED_LATTICE) -> functor (E : Interface.EQ with type t = L.t) -> sig ... end

module Distributive_Lattice : functor (L : Interface.DISTRIBUTIVE_LATTICE) -> functor (E : Interface.EQ with type t = L.t) -> sig ... end

module Bounded_Distributive_Lattice : functor (L : Interface.BOUNDED_DISTRIBUTIVE_LATTICE) -> functor (E : Interface.EQ with type t = L.t) -> sig ... end

module Heyting_Algebra : functor (H : Interface.HEYTING_ALGEBRA) -> functor (E : Interface.EQ with type t = H.t) -> sig ... end

module Involutive_Heyting_Algebra : functor (H : Interface.HEYTING_ALGEBRA) -> functor (E : Interface.EQ with type t = H.t) -> sig ... end

module Boolean_Algebra : functor (B : Interface.BOOLEAN_ALGEBRA) -> functor (E : Interface.EQ with type t = B.t) -> sig ... end

module Semiring : functor (S : Interface.SEMIRING) -> functor (E : Interface.EQ with type t = S.t) -> sig ... end

module Ring : functor (R : Interface.RING) -> functor (E : Interface.EQ with type t = R.t) -> sig ... end

module Commutative_Ring : functor (R : Interface.COMMUTATIVE_RING) -> functor (E : Interface.EQ with type t = R.t) -> sig ... end

module Division_Ring : functor (R : Interface.DIVISION_RING) -> functor (E : Interface.EQ with type t = R.t) -> sig ... end

module Euclidean_Ring : functor (R : Interface.EUCLIDEAN_RING) -> functor (E : Interface.EQ with type t = R.t) -> sig ... end

module Field : functor (F : Interface.FIELD) -> functor (E : Interface.EQ with type t = F.t) -> sig ... end

module Invariant : functor (I : Interface.INVARIANT) -> functor (E : Interface.EQ1 with type 'a t = 'a I.t) -> sig ... end

module Contravariant : functor (C : Interface.CONTRAVARIANT) -> functor (E : Interface.EQ1 with type 'a t = 'a C.t) -> sig ... end

module Profunctor : functor (P : Interface.PROFUNCTOR) -> functor (E : Interface.EQ2 with type ('a, 'b) t = ('a, 'b) P.t) -> sig ... end

module Monad_Zero : functor (M : Interface.MONAD_ZERO) -> functor (E : Interface.EQ1 with type 'a t = 'a M.t) -> sig ... end

module Monad_Plus : functor (M : Interface.MONAD_PLUS) -> functor (E : Interface.EQ1 with type 'a t = 'a M.t) -> sig ... end

module Extend : functor (X : Interface.EXTEND) -> functor (E : Interface.EQ1 with type 'a t = 'a X.t) -> sig ... end

module Comonad : functor (C : Interface.COMONAD) -> functor (E : Interface.EQ1 with type 'a t = 'a C.t) -> sig ... end

module Bifunctor : functor (B : Interface.BIFUNCTOR) -> functor (E : Interface.EQ2 with type ('a, 'b) t = ('a, 'b) B.t) -> sig ... end

module Bicontravariant : functor (B : Interface.BICONTRAVARIANT) -> functor (E : Interface.EQ2 with type ('a, 'b) t = ('a, 'b) B.t) -> sig ... end