A Metamath verifier in Scala
Scala
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.settings
src/main/scala/org/metamath/scala
.classpath
.gitignore
.project
LICENSE
README.md
build.sbt

README.md

mm-scala

This is intended to be a lightweight version of mmj2 which is optimized for rapid development. (In other words, the errors are probably not so great but the code is relatively short.) I don't think this is likely to become a full-featured proof assistant, but it does more complete parsing than any other verifier except metamath.exe. In particular, it will read $t and $j comments, and checks that typecodes have been defined before they are used.

This is a 100% grammatical verifier - it parses all formulas, and does not use strings during verification. Verification of non-grammatical databases is not planned.

Future additions include maintenance utilities such as proof replacement.