Proving Axiom Correct. COQ/Axiom type matching

Tim Daly <[email protected]>
Newsgroups gmane.comp.mathematics.axiom.devel
Message-ID <CAJn5L=LzJje2cjk4uSsDQKHERhLAyvM1PRQcC+SAAy43hLKQ7w@mail.gmail.com> 
COQ defines some primitive types. For example, it defines 'nat' which
is the type
of 'natural numbers'.

The corresponding type in Axiom seems to be NonNegativeInteger. At the moment
it seems interesting to try to unify these two types, allowing
primitive Axiom operations
to be expressed in COQ directly.

Unifying base types will allow easier translation of Axiom's algorithms.
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.