Thierry, that's a cool project, I had no idea it exists. I took a brief look at the syntax and the currently implemented tactics. The "equality" tactic looks very useful, others are a bit too technical for me to understand. Correct me if I'm wrong, but it should be possible to write a tactic for expanding polynomial expressions, and maybe to port Mario's tactic for long addition and multiplication.
I agree that one would need a more powerful language to implement some of the more interesting tactics. The "improve" tactic from metamath exe seems as one example. I'm not sure if it's beneficial to come up with your own scripting language for tactics, but if I were to use a library to write a tactic, I would certainly prefer to have functions from your language like matching patterns etc. -- 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/b1dbfee5-d920-407a-b452-2cc952e179a3n%40googlegroups.com.
