Skip to content
Lean type-checker written in Scala.
Scala
Branch: master
Clone or download

Latest commit

Files

Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
project Update dependency versions. Jun 16, 2018
src Switch to hand-rolled parser. Feb 3, 2018
.gitignore
COPYING Add license. Jul 29, 2017
README.md Remove to-do item. Mar 19, 2017
build.sbt Update dependency versions. Jun 16, 2018

README.md

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.
You can’t perform that action at this time.