/lang-metamath

Use Metamath through a Racket library and language, and DrRacket IDE support

#lang metamath & a Racket-based Metamath IDE

This might grow into:

  • A Racket-based parser for set.mm and other Metamath databases
  • ...which reads the axioms and theorems into executable data structures that build only valid proofs
  • ...with interactive tools in the DrRacket IDE
  • ...where most of the proofs are written as calculational / equational proofs.