The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

I am confusing between definition and fixed point

And between axiom reserved keyword and definition reserved keyword

Can axiom be used in eval ? 

If not , what is axiom used for in programming coq

I find a paper that can auto generate fixed point, 

I am curious to know whether coq have command to generalize axioms into a function

If not, do this idea exist in application? 

If exist, what kind of rules need to apply in order to generalize into a function from axioms.

Sent from Outlook Mobile

On Sun, Feb 7, 2016 at 8:37 AM -0800, "Pierre Casteran" <pierre.casteran AT labri.fr> wrote:

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