Proving Axiom Correct. COQ/Axiom type matching

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

Proving Axiom Correct. COQ/Axiom type matching

Tim Daly
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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer