trepplein: a Lean type-checker

Lean is an interactive theorem prover based on dependent type theory. For additional trust, Lean can export the generated proofs so that they can be independently verified. Trepplein is a tool that can check these exported proofs.

Trepplein is written in Scala, and requires SBT to build.

sbt stage
./target/universal/stage/bin/trepplein .../export.out

Other checkers

• tc, a type-checker written in Haskell.
• leanchecker, a bare-bones version of the Lean kernel.