Metamath in STELF

Metamath is one of the largest projects wrt proof verification. We formalize a portion of that here as a proof of concept for the utility of the new STELF system.

Building

1. Install STELF
2. Clone this repository
3. Run stelf check stelf.toml (to check) or stelf repl stelf.toml (for REPL)

Enjoy!

Features highlighted

• Firstly literally highlighted if you use Zed or Nvim is the text, and if you're terminal has tty enabled, then the output will also be highlighted.
• Enjoy the new syntax
  • -> as a name
  • %proof for what used to be %sort + %term + %mode + %worlds + %total
  • A finished module system
  • Structured programs, better configs
• Literate programming While this uses Markdown, we can also use latex, or any other format we'd like (the plugins can't highlight them all, but can highlight any of typst html, org rst rtf javadoc jsdoc doxygen and asciidoc (made possible by language injections))