> Hi Gino, > Is there a "formal" definition of tactic? I'm afraid I can't be of much help here, since I'm just the end user. For a formal definition you're probably better off asking the experts (Thierry, Mario etc.). In the MM1 description https://github.com/digama0/mm0/blob/master/mm0-hs/mm1.md it's mentioned that its tactics language is close to Scheme (in the Lisp family), so that could be a starting point to find useful sources.
Quote: <<The key new capability of MM1 over MM0 is the inclusion of a Turing-complete programming language over MM0, a lisp dialect similar to *Scheme* <https://schemers.org/>. Proofs of theorems are given as s-expressions, which may be constructed by lisp programs, also known as "tactics" in this context.>> > In https://github.com/metamath/metamath-knife/issues/87 Mario pushed back on the idea of having metamath-knife supporting Work Variables, I'd need to dig up the proposal made at that time and see what can be done. I won't hide that support for work variables would make me very happy, but if it doesn’t pan out, well.. I did my best :) -- 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 visit https://groups.google.com/d/msgid/metamath/ac38cdaa-b320-4bf2-899f-e0e69bb65b97n%40googlegroups.com.
