I'm a bit late to the discussion, but do I understand correctly that this new community verifier is supposed to be a spin-off to MM0/MM1 project? In particular, MM1 code base will be the starting point, proofs won't look like mmj2's proof sheets, and most of tactics/automation will be written in a custom language (as I understood, MM1 uses a scheme-like language)? Also as far as I understand this new verifier should be able to replace an ensemble of tools we use now for CI (or is this a separate project which will include support for ungrammatical databases?).
When I first read this thread, I imagined the project roughly as depicted on Thierry's diagram (a universal core library agnostic of grammar, tactic language etc + PA program using that lib to imitate mmj2 or imitate MM1 and so on), but on the second reading I got the impression that the underlying idea was to base it of MM1 from the beginning. I'm not sure if this is a source of confusion for others, but it is definitely for me, so it would be nice if the intended connection between MM0/MM1 and the new verifier could be clarified. суббота, 28 ноября 2020 г. в 06:42:10 UTC+7, [email protected]: > It's certainly possible to have pages for terms and definitions, but I > don't have much to show for them beyond what's already on the index page. > If I can figure out how to do pretty printing with embedded links, I can > also link all the uses of a symbol so that you can click on a "+" anywhere > to go to its definition (or at least to the page that says they are an > axiomatic term constructor with no definition). > > On Fri, Nov 27, 2020 at 4:51 PM Glauco <[email protected]> wrote: > >> >> I guess there's the concept of "definition" for those terms(?) : can it >>> be rendered in a linked html page? >>> >> >> Browsing this page >> https://digama0.github.io/mm0/peano/index.html >> I may be wrong, but it looks like "nat" and "+" in Peano are not >> eliminable, kind of "e." is not eliminable in ZF , so my question is >> probably ill-posed >> >> -- >> 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/6a622530-e403-43d0-962d-8526bd54e1e8n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/6a622530-e403-43d0-962d-8526bd54e1e8n%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 on the web visit https://groups.google.com/d/msgid/metamath/049f0304-73fe-4a93-a2c3-2a2da3a62e0dn%40googlegroups.com.
