文件名称：nbe-for-mltt:通过评估对马丁·洛夫类型理论进行归一化
文件大小：28KB
文件格式：ZIP
更新时间：2024-06-12 03:22:09
OCaml
恩贝特·姆利特 通过评估实现马丁-洛夫类型理论的归一化，包括相关乘积（pi），相关总和（sigma），自然数和累积层次结构。 此实现可正确处理pi和sigma的eta。 此实现也已扩展为包括基于Coquand语义类型检查器的类型检查器。 因此，为了与规范化程序进行交互，可以编写一个文件，其中包含用于规范化各种术语的定义和命令的列表。 例如： let plus : Nat -> Nat -> Nat = fun m -> fun n -> rec n at x -> Nat with | zero -> m | suc _, p -> suc p let fib : Nat -> Nat = fun n -> let worker : Nat * Nat = rec n at _ -> Nat * Nat with | zero -> <1
【文件预览】：
nbe-for-mltt-master
----.gitignore(2KB)
----README.md(2KB)
----test()
--------eta.tt(288B)
--------fib.tt(399B)
----nbe-explanation.md(23KB)
----check-explanation.md(458B)
----normalize_lib.opam(526B)
----mltt.opam(458B)
----src()
--------bin()
--------lib()
----dune-project(35B)
----Makefile(220B)