coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. |
- [Coq-Club] Abstract Reasoning with Coq, Jevgenijs Sallinens
Archive powered by MhonArc 2.6.16.