On 31/03/17 05:34, Tim Daly wrote:
Consider the Axiom Domain NonNegativeInteger. NNI roughly
corresponds to the Type theory "Nat" construction. They differ
in that Axiom uses Lisp Integers whereas Type theory uses
Peano arithmetic (a zero and a successor function) but for
our purposes this does not matter at the moment.
Perhaps there are issues around this that will matter? Given that there
are two formulations of each algebra, one like this:
zero: () -> $
succ: ($) -> $
and one like this:
+ ($,$) -> $
If one form is needed for inductive proofs and the other form for
applied mathematics. Could Axiom hold both forms in a single
category/domain and switch between them as needed?
Martin
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
