Hmm. The problem to be solved involves several parts.
Idris is of interest in PART 6, 7, and 8 below.
PART 1: We have the domain
We have GCD in NAT (axiom: NonNegativeInteger or NNI)
NonNegativeInteger is what Axiom calls a "Domain", which means
that it contains signatures, such as
quo : (%,%
On 21/09/2019 13:40, Henri Tuhola wrote:
The elaborator reflection also allows accessing the term rewriting. I
suppose that's all you need in order to write a program that
simplifies equations inside the type context?
I am trying to understand if these equations could be solved in this way?
I
Idris has a way to present equalities like this:
addition_unit : (a:Nat) -> (a + 0) = a
addition_s : (a,b:Nat) -> (a + S b) = S (a + b)
add_commutative : (a,b:Nat) -> (a + b = b + a)
They can be used to prove more things:
try_out : (x,y:Nat) -> ((x + 0) + y) = y + x
try_out x y = rewrite additio
I'm a fan of both Axiom and Idris. I think my ideal would be Axiom
mathematics build on top of the Idris type system.
The Axiom type system was incredibly advanced for its time but I suspect
the Idris type system has finally caught up and overtaken it? Correct me
if I'm wrong but I think the A
