The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi Martin,

  What is really your question?

  The code you sent is not even accepted by the Coq system
  Please look at the type error message you've certainly got at the  
third line; you will understand
that it is impossible for us to answer.

  It is important to begin to study Coq with the help of some tutorial.

  About your last question about Ring, there is a lot of  
documentation about that in the reference manual.

Pierre






Quoting Mandy Martino 
<tesleft AT hotmail.com>:

> Hi ,
>
>
> Require Import Arith.
> Parameter G : Type.
> Axiom reflexive : forall x y z:G, x <= x.
> Axiom symmetric : forall x y z:G, x = y <= y = x.
> Axiom transitive : forall x y z:G, (z = y) * z <= (z = x) * x.
>
>
> Regards,
>
> Martin