Классы RelationClasses и CRelationClasses

Question

Стандартная библиотека Coq имеет два подмножества модулей классов, один из которых привязан к Coq.Classes.RelationClasses, а другой к Coq.Classes.CRelationClasses.Последнее, похоже, было добавлено совсем недавно (2012).

Я, должно быть, упускаю что-то очевидное, поскольку они оба выглядят очень похожими на меня.

В чем причина их существования?

Answer 1

Основное различие заключается в типе отношений, которые они поддерживают:

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

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