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 _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
