Hi Olivier, Very interesting! Mathjax is also what I’m using for the rendering of the “structured” pages, like:
http://metamath.tirix.org/esum.html http://metamath.tirix.org/areacirc.html I’m maintaining the rules for translating any set.mm statement into MathJax here: https://github.com/metamath/set.mm/blob/develop/set-mathml.mmts Feel free to reuse it! It looks like for simplifying a formula, one would start at the lowest level, and then continuously work ones way up: If I’m looking for a proof assistant, I would probably like to have this automated, and the whole formula simplified in one step. But I suppose for educational purposes, you want to expose each of these steps. BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/C8EB3D1C-A245-4A47-9D8E-44F335939C26%40gmx.net.
