Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Abstract Reasoning with Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Abstract Reasoning with Coq


chronological Thread 
  • From: "Jevgenijs Sallinens" <jevgenijs AT dva.lv>
  • To: <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] Abstract Reasoning with Coq
  • Date: Sun, 14 Mar 2004 17:16:36 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Coq users,
Please refer to my web site www.mathcoq.dva.lv for Coq8.0 beta  modular development, devoted to abstract reasoning with  Peano and binary natural numbers. In particular, this development  demonstrate,  how to use modules of Peano numbers to derive results for binary numbers. Also some general forms of induction principles and recursion operators are introduced and demonstrated to derive some recursion operators on two arguments.
Documentation is  very poor at the moment. Here attached very simple kind of an abstract in plain text.
I will be very interested in any kind of discussion or cooperation.
 
Regards,
Jevgenijs Sallinens.  



Archive powered by MhonArc 2.6.16.

Top of Page