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

[Martin Baker]

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