Hey Antony, While we're talking about unifiers, I'm still in the market for one which is api based with a thin command line wrapper.
Could you elaborate on your proposal a bit? When you say "thin command line wrapper", do you mean a fully functional proof assistant (like a minimalist metamath.exe) or simply a command line tool that let's you call the proof assistant functionality (unify step, renumber, etc.)? 3. A unifier api would allow a programmer to focus on the front end of a proof assistant (my personal conceit, since 2018, is that I'd like to see/write an Incredible Proof Machine <https://incredible.pm/> (vertex-edge-graph drag and drop toy proof assistant) with a Metamath back end, and, oh, maybe a maxGraph <https://www.npmjs.com/package/@maxgraph/core>front end). Another interesting proposal. Are you suggesting a drag and drop proof assistant where the proof lines are represented as vertices and hypothesis dependencies as edges? What would the advantage of such a proof assistant be in your opinion? Until the end of October I'll still be busy with the first version of mmt1 (the proof assistant I am currently developing) and if there is interest from people in using mmt1 I'll probably be busy until next year developing future versions of mmt1. But after that I would be open to new ideas if you need any help. Best regards, Marlo Bruder -- 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/6aee9aff-7d6c-410f-9aaa-73b758f28e07n%40googlegroups.com.
