Axiom has type information everywhere. It is strongly
dependently typed. So give a Polynomial type, which
Axiom has, over a Ring or Field, such as
Polynomial(Integer) or Polynomial(Fraction(Integer))
we can use theorems from the Ring while proving
properties of Polynomials.
Axiom has a deep type h
I doubt it does cover that. And I think there would be at least two
approaches to implement GCD for polynomials in Idris.
Obvious approach would be to construct a type that represents
polynomials on some base number and variables. For example,
(Polynomial Nat [X]). You would then prove GCD for thi
Does the Idris code cover GCD for polynomials?
On 9/20/19, Henri Tuhola wrote:
> You can already define and prove gcd in idris/agda/coq. It's not too hard
> either.
>
> This weekend I am trying to prove transitive closure can be computed in
> Idris. The way I represent it is that I have f:(a ->
You can already define and prove gcd in idris/agda/coq. It's not too hard
either.
This weekend I am trying to prove transitive closure can be computed in
Idris. The way I represent it is that I have f:(a -> a -> Type), this forms
a type that is inhabited when a statement is true. I can wrap this i
