Re: [Axiom-developer] Axiom Sane musings (SEL4)

[Henri Tuhola]

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 this structure.

Another approach I can think of would exploit the way how
type-propositions themselves can cause computer-algebra-system -like
behavior, reusing variables that the type system is already working
with. You can prove (a = b) -> (b = c) -> (a = c), then compose
equations together with that. Similarly you can rewrite x to y inside
a type if you have (x = y). There's already some support for changing
the behavior of Idris type checker, it could be that some sort of
equation simplifier could be implemented with features that Idris
already has.

-- Henri Tuhola