This repository includes:
- a specification for a tactics-based proof language for Metamath,
- a reference implementation in Rust for building Metamath proofs with that language,
- a set of tactics for building proofs for the ZFC set.mm Metamath database
- a few example proofs
Rumm intends to be simple, generic and yet powerful. Simple in the sense that it only specifies a very limited set of built-in tactics. Generic in the sense that the language itself is not taylored to any specific Metamath database, but can be reused for all of them.
At the origin it intends to answer the feasibility question "what would a tactics-based language for Metamath look like?".