The Coq mailing list

[Victor Porton <porton AT narod.ru>]

<<<
Class Base := {
  set: Set
}.

Class Relation := {
  base :> Base;
  graph: set->set->Prop
}.

Class Reflexive := {
  relation :> Relation;
  is_reflexive: forall x:set, (graph x x)
}.

Class Symmetric := {
  relation :> Relation;
  is_symmetric: forall x y:set, ((graph x y)<->(graph y x))
}.
>>>

Compilation output:
File "/home/porton/t/test.v", line 15, characters 0-107:
Error: relation already exists.

This is because I used the id [relation] two times.

What is the suggested naming conventions for names of base classes in Coq?

I's like to see my theory rewritten in such a way to demonstrate the 
suggested naming conventions.

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