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. _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
