The Coq mailing list

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

Dear Coq Users,

At my home page http://jevgenijs.sallinens.dva.lv there is available information about new Coq 7.4 development devoted to modular axiomatic approach to the theory of natural numbers.
Please consult Compile.txt file for compilation.
Main idea was to replace Coq inductive/recursive definitions by some constants (parameters and axioms), so that abstract reasoning, independent on underplaying implementation of natural numbers, became available. I hope also that methodology used for modules and module types will be interesting for many users.
Similar development for lists and general operators for complicated iterations and recursions will be available at the same page within month or two.
I will be glad to receive comments, suggestions and proposals (e-mail: jevgenijs AT dva.lv). Especially I am interested on resolving the problem of huge file (3 MB) created after compilation of the example combining all of involved modules (file test.v).
I don't know if some Coq inefficiency involved or I should use modules in some different way to avoid such problems.

Best Regards,
Jevgenijs Sallinens, Riga, Latvia.

________________________________________________
Message sent using UebiMiau 2.7.2