a Nim verifier (and yamma's MmParser.ts)

[Glauco]

Hi everyone,

I’d like to suggest a couple of possible new entries for the Metamath verifiers page:

1. Forematics
   I recently stumbled upon this post from 2021 on the Nim forum:
   Show Nim: Forematics is a Metamath verifier written in Nim.

   At the time of the post, Lean was listed at 61 on the 100-theorem list; today, it's at 79.

   • Forematics appears to be a Metamath verifier implemented in Nim.
   • The project has a GitHub repository, which currently has 20 stars.

   I haven’t personally tried it, but it might be worth reviewing and potentially adding to the verifiers list.

2. Yamma
   Yamma uses the MmParser.ts class as its .mm parser verifier. It’s currently not listed on the verifiers page, but you can consider adding it if appropriate.

Glauco

[Jim Kingdon]

Sounds good to me. You should be able to make a pull request to https://github.com/metamath/metamath-website-seed/blob/main/other.html .

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/d7afc7df-8475-434d-8700-12deb6c482c1n%40googlegroups.com.

[Glauco]

Thanks for the reply and for the link, Jim

I'll give setting up a Nim environment a shot (though I must admit I don't have any prior experience with it) and see if I can test it against the .mm test file suite.

Alternatively, I might try reaching out to the author of Forematics, even though it's a project from four years ago.

Glauco