coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to prove and evaluate new function definition with this axioms

From: "John Wiegley" <johnw AT newartisans.com>
To: Mandy Martino <tesleft AT hotmail.com>
Cc: Pierre Casteran <pierre.casteran AT labri.fr>, "coq-club\@inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] how to prove and evaluate new function definition with this axioms
Date: Tue, 09 Feb 2016 10:30:23 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f170.google.com
Ironport-phdr: 9a23:9lsFxBKMs34putTn79mcpTZWNBhigK39O0sv0rFitYgVKPrxwZ3uMQTl6Ol3ixeRBMOAu60C0LKd7PyocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0ILsj6vtp9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DzKSweerl4VSHkXlB0AVxTI9xX3UIvZsizms+N83G+ROsigHoo5QTCz06A+Aj3viCFPCD80/2Xam4Y42KBcoBS+jxpy3IfOfICOPfxlOKjaeIVJa3BGW5MbdStBBMuDboYAC+cQd64MrY79oUQmqxahDBOwBfjmzCQOjXjzi/5pm989GB3LiVRzV+kFt27Z+ZCsbP8f
Organization: New Artisans LLC

>>>>> Mandy Martino
>>>>> <tesleft AT hotmail.com>
>>>>> writes:

> I am confusing between definition and fixed point

Questions like this are clearly answered by progressing through a tutorial
text, such as Software Foundations:

https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

> If not , what is axiom used for in programming coq

It would be more appropriate to ask this nature in a more beginner-focused
medium, such as the #coq IRC channel on irc.freenode.net, which Adam proposed
earlier.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/07/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/07/2016
- Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Pierre Casteran, 02/07/2016
  - Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, Mandy Martino, 02/09/2016
    - Re: [Coq-Club] how to prove and evaluate new function definition with this axioms, John Wiegley, 02/09/2016