精益>> trepplein>> 返回
项目作者： gebner

项目描述 ：
用Scala编写的精益类型检查器。
高级语言： Scala
项目地址: git://github.com/gebner/trepplein.git
创建时间： 2017-03-06T09:44:43Z
项目社区：https://github.com/gebner/trepplein
开源协议：Apache License 2.0
下载


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.

  1. sbt stage
  2. ./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.