For Glauco, and anyone else interested in how a simple API for performing unification might be specified, please find the promised spec in this repo:
https://github.com/Antony74/yamma-unifier-cli I hope that is helpful, and I'm happy to receive feedback if it could be more so. I've written the command line interface (CLI) too - the API is mocked so it all runs but there's just the one file that can be unified (via hardcoding) at the moment. I'm tempted to add code to create requested .mmp files from .mm files, as I don't believe yamma can do that yet? That would be horribly inefficient because I'd be using a different parser... well, verifier actually, which would make it even less efficient, but I think it would be quite easy to write. Best regards, Antony On Sun, Sep 28, 2025 at 12:12 PM Glauco <[email protected]> wrote: > Hi Antony, > > I'm a bit busy, but if you have the time to write the spec of the API, it > would be helpful. > > Just a couple of unit tests in any language would probably be enough for > us to understand the goal. > > BR > Glauco > > -- > 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/33412bc3-bde8-489a-a69b-ed6fa7f0b958n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/33412bc3-bde8-489a-a69b-ed6fa7f0b958n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAJ48g%2BDf8m1aAaQtECMC_CL%2BCSpSfjrvrBAY4NnP%2Btgktf8wdQ%40mail.gmail.com.
