Hi Mario, it'd be great if you could record a session where you start from set.mm.mm0 and write a MM0 proof.
I'm particularly interested in seeing how the autocomplete (ctrl+space) and the "Go to definition" work. Can you please remind me the kind of "notations" needed to translate from mm to mm0 ? An example ? Glauco Especially if you mean the end to end MM workflow, a lot of this is still > very much a dream/plan/roadmap and not a current reality. What I can show > you now with mm0-rs is the use of MM1 to construct a .mmb binary proof file > that can be verified by external MM0 verifiers like mm0-c. I can probably > declare a few notations and do the same thing starting from set.mm.mm0, but > the result will still be an MM0 proof, not an MM proof. That's what the > plan is all about. > > 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/5a4c3b94-f61d-4c30-99c9-0d5382a3dc74n%40googlegroups.com.
