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 think Axiom equation solving tends to work in terms of reals and
complex numbers. I suspect that a type that depends on a floating point
literal would be problematic in that the equality could fail due to a
rounding error.
Also, although I never understood it, I get the impression that Axiom
equation solving is extremely complicated. First representing it as
functions within polynomials within functions an so on, then expressing
the multivariate polynomials in terms of a single variable. I've
probably got this all wrong but the point is: could elaborator
reflection handle this level of complexity?
If these kinds of thing can't be done in the type system then I guess
they would have to be handled differently from equations in proofs.
Martin
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
