trivial-rs

A parser for the Metamath Zero binary proof format

A Metamath Zero kernel for Trivial

Utility tools for Metamath Zero binary proof files

The Trivial proof verifier - an interface to the Metamath Zero kernel

The Trivial compiler framework for Metamath Zero binary proofs

Definitions of opcodes present in the Metamath Zero binary format