On Fri, Oct 18, 2019 at 5:21 AM Olivier Binda <[email protected]> wrote:
> I do a lot of cow boy coding and nothing is set in stone but : > > 1) I would like to start looking into mm0 and building Mephistolus over mm0 > (because at one point, I will want user to be able to add definitions of > their own and I will need the added soundness, as well as the simpler > parsing, and maybee other stuff that I don't understand yet) > > Also, by building mephistolus on mm and mm0, It'll become more generic and > probably better (closer to true maths). > Assuming you have a program that thinks for a while and spits out theorem references, you can probably create a .mmu file without too much effort. This is a very simple lisp s-expression syntax for MM0 proofs, which is probably a lot easier to work with than the binary format. Unfortunately, the .mmu examples on the web page are out of date. The previous version had some nontrivial parsing stuff (keywords, punctuation) and now it's all (pure (s-expressions) (like (this))) to keep it simple. Alternatively, if you have an MM exporter already, you can just run the resulting .mm file through the MM -> MM0 translator. One new option in MM0 (rather MM1) is that you could write your program *in* MM1. This is reasonable for simple programs that do pattern matching and such but if it's really complicated it might be a performance problem (plus it's untyped so it's probably not a good idea to write a huge amount of code in it). You should also be able to call Mephistolus from MM1, although the infrastructure for that isn't built yet. Ask me if you have any questions. Mario -- 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/CAFXXJSuy0F53%3DToZwW_TZxajMtFvNt2aJ%3D%2ByWWB%3DgzPx12Vvmw%40mail.gmail.com.
