Done.
On Saturday, May 8, 2021 at 7:43:46 PM UTC-4 di wrote:
> 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).
>
--
You received this message because
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 wrote:
> If what you mean is the link in the list of verifiers, I
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 di@gmail.com wrote:
> It's still basically in one file, although now that file is
>
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
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
