> > > > Alternatively, if you have an MM exporter already, you can just run the > resulting .mm file through the MM -> MM0 translator. > > Indeed. I might be able to do this on the resulting mm proof to turn it into a mm0 proof. But I would rather have high level proofs of Mephistolus Theorems based on mm0 theorems.
Or, it might also be possible to import mm0 (or mm) theorems as Mephistolus theorems and Have Mephistolus be self reliant, with it's own set of axioms. But by doing this, I would lose a very valuable asset : metamath and it's worldwide experts that constantly improve the way metamath describes math. I have started looking at the Peano file and understanding mm0. This looks a lot like function signatures, with abstract/concrete bodies. So Mephistolus statements like "( v1w -> v2w )" might be viewed as a function im (v1w v2w : wff) : wff = $( v1w -> v2w )$ ... looking further into it... -- 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/9371b179-2040-4f51-a376-ba0e970b244c%40googlegroups.com.
