The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The following does not compile:

Classes.v:
[[[
Class Base {set: Set} := {
}.
]]]

RelTypes.v:
[[[
Require Import Classes.
Require Import sset2.

Class Relation {set: Set} := {
  relation_is_base :> @Base set;
  mygraph: Set; (*mygraph: set->set->Prop*)
  is_rel: is_graph mygraph;
  is_inside: sub mygraph (product set set)
}.

Definition compose_relation_classes {set:Set} (f g: @Relation set) := 
Build_Relation(compose_graph (@mygraph set f) (@mygraph set g)).

Class Reflexive {set: Set} := {
  reflexive_is_relation :> @Relation set;
  is_reflexive: forall x, ((inc x set)->(related mygraph x x))
}.

Class Symmetric {set: Set} := {
  symmetric_is_relation :> @Relation set;
  is_symmetric: forall x y, ((related mygraph x y)<->(related mygraph y x))
}.

Class Transitive {set: Set} := {
  transitive_is_relation :> @Relation set;
  is_transitive: compose_relation_classes transitive_is_relation 
transitive_is_relation = transitive_is_relation
}.
]]]

The trouble is that there are seemingly no way to call 
compose_relation_classes from inside Transitive, because a condition for a 
class cannot refer to that class as a whole rather than as individual fields.

In my opinion, we need a new keyword to refer to the current instance of a 
class, like "this" in C++ or "self" in Python.

-- 
Victor Porton - http://portonvictor.org