Hi Mario, I am intrigued by your work toward translating from MM0 to HOL or a subset thereof, as you discuss in your post of May 19: ( https://groups.google.com/d/msg/metamath/raGj9fO6U2I/8gKq_KFuBQA), and I would like to understand better how the incoming MM/MM0 statements correspond to their HOL counterparts. The question that always comes to my mind is what statements in Metamath (normally theorems) translate into.
You mention OpenTheory as a target, so I imagine the language of statements to be a pretty generic language of the HOL variety. Can you offer some combination of description and examples of how the translation of a Metamath statement relates to the original (or MM0) version of the statement? This would be very much appreciated. I have some notions of how this might go, and will be very interested to learn of your actual practice. -Cris -- 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/CAOoe%3DWLnpy%3D1wF1Sh8hOrpjOBcDzj5Ssty7hfwWJLWVwhfPuXA%40mail.gmail.com.
