[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Proving Axiom Correct. COQ/Axiom type matching
From: |
Tim Daly |
Subject: |
[Axiom-developer] Proving Axiom Correct. COQ/Axiom type matching |
Date: |
Fri, 30 Dec 2016 18:09:39 -0500 |
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.
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Axiom-developer] Proving Axiom Correct. COQ/Axiom type matching,
Tim Daly <=