On Tue, Jan 14, 2025 at 5:49 PM Gino Giotto <[email protected]> wrote:
> > 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 :) > (Note: I have been on holiday since christmas, so sorry for any delayed responses and feel free to re-ask any questions which I missed.) Just to clarify on the above point: I was not advocating against work variables (metavariables) in metamath-knife, I was advocating against metavariable support in the `Formula` type that mm-knife uses for completed proofs. I think metavariables and other proof assistant features should be supported via another type e.g. `MetaFormula` which is a superset of `Formula`. The data structures you want to use for in-progress proofs are rather different from what you use for completed proofs. But as a result of that, a module for handling MetaFormulas would be essentially a separate thing from the rest of mm-knife, and it's not yet clear whether there are benefits for having it in mm-knife itself, compared to if it was a data type defined by a downstream crate with its own concepts of elaboration and tactic execution (which interact with unification etc and need to use MetaFormulas in a variety of ways). -- 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/CAFXXJSsoCdpz3rzz7_pXCEKosrp3bnJkLqk_fMJ1R0KF5G_Fhw%40mail.gmail.com.
