A tool for mechanically checking natural deduction proofs in first order logic with equality over the simply typed lambda calculus.
Accepts a list of claims, where each claim is either an inference rule, a theorem, or a type declaration, and checks that all proofs are correct and types are consistent.
Plays well with markdown.