文件名称：type-theory:Haskell通过评估和双向类型检查实现归一化
文件大小：9KB
文件格式：ZIP
更新时间：2024-04-09 01:51:48
Haskell
类型理论 Haskell通过评估和双向类型检查实现归一化 用cabal run 。在GHC 8.10.4上进行了测试，可能与其他人一起使用。 示例代码： nat = ^t:*.(t->t)->t->t : * 2 = \t f x.f (f x) : nat 4 = \t.2 (t->t) (2 t) : nat
【文件预览】：
type-theory-master
----LICENSE(1KB)
----Parser.hs(3KB)
----Typechecker.hs(3KB)
----Setup.hs(46B)
----Repl.hs(2KB)
----Term.hs(2KB)
----.gitignore(15B)
----type-theory.cabal(863B)
----CHANGELOG.md(114B)
----Erase.hs(2KB)
----README.md(281B)
----Main.hs(239B)
----NbE.hs(2KB)
----TypedTerm.hs(1KB)