Search code examples
coq

RelationClasses versus CRelationClasses

The Coq standard library has two subsets of classes modules, one anchored in Coq.Classes.RelationClasses and the other in Coq.Classes.CRelationClasses. The latter seems to have been added more recently (2012).

I must be missing something obvious as they both look very similar to me.

What is the reason they exist?

Solution

  • The key difference is in the type of relations they support:

    (* RelationClasses, actually defined in Relation_Definitions *)
Definition relation (A : Type) := A -> A -> Prop.

(* CRelationClasses *)
Definition crelation (A : Type) := A -> A -> Type.