Could you update the name of the verifier to "mm-lean4"? "Metamath.lean" is a bit generic (file names in lean 4 have to follow some package-oriented naming conventions like in java).
On Sat, May 8, 2021 at 7:38 PM Norman Megill <[email protected]> wrote: > If what you mean is the link in the list of verifiers, I updated it: > http://us2.metamath.org/other.html#leanmmverify > > Norm > > On Saturday, May 8, 2021 at 7:13:01 PM UTC-4 [email protected] wrote: > >> It's still basically in one file, although now that file is >> https://github.com/digama0/mm-lean4/blob/master/Metamath/Verify.lean . >> Probably better for the metamath site to point to the repo >> https://github.com/digama0/mm-lean4/ instead though. >> >> The other file is WIP at the moment, but it now contains some really >> interesting stuff about a deep embedding of metamath (i.e. appendix C). In >> particular, I finally managed to prove the theorem that I got stuck on with >> "metamath in metamath", namely the admissibility of cut. That is, in >> appendix C there is a definition of the closure of a formal system under >> applications of axioms; I proved that you can also apply a theorem instead >> of an axiom. This is of course very important for verifiers, which apply >> both theorems and axioms when deducing new theorems, even though >> provability is defined only with respect to applications of axioms. >> Although now that I think of it I haven't proved anything about the >> "reduct" operation, which verifiers also rely on... >> >> Mario >> >> On Sat, May 8, 2021 at 6:08 PM vvs <[email protected]> wrote: >> >>> Good news! >>> >>> This project moves so fast, that some people even expect that it will >>> soon support LSP, apparently. Indeed, the source file is no longer >>> self-contained. I guess that URL announced on Metamath site needs fixing >>> already :) >>> >>> -- >>> 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/f22c9d81-ec51-4337-aa8f-2884e7cf1e58n%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/f22c9d81-ec51-4337-aa8f-2884e7cf1e58n%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/f2fa7ec1-7a3d-4e7d-9f65-d152c5124675n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f2fa7ec1-7a3d-4e7d-9f65-d152c5124675n%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/CAFXXJSsCsx%2Bkxj9oWDbTDmwZNB38XpoDMH-V66ax8%3DJ0wRwDjA%40mail.gmail.com.
