Module AAC_coq.Classes

module Classes: sig .. end

Coq typeclasses

val mk_morphism : Term.constr -> Term.constr -> Term.constr -> Term.constr

val mk_equivalence : Term.constr -> Term.constr -> Term.constr

val mk_reflexive : Term.constr -> Term.constr -> Term.constr

val mk_transitive : Term.constr -> Term.constr -> Term.constr