The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

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.