文件名称：hstar:无意类型的λ-联合演算
文件大小：73KB
文件格式：ZIP
更新时间：2024-05-20 12:02:12
Coq
Kong洞 文件 10 | [BohmTrees](src/BohmTrees.v) 10 | [Types](src/Types.v) 8 | [LeastFixedPoint](src/LeastFixedPoint.v) 7 | [TypeConstructor](src/TypeConstructor.v) 6 | [Compile](src/Compile.v) 6 | [StrongConstructor](src/StrongConstructor.v) 5 | [Annotate](src/Annotate.v) 4 | [Codes](src/Codes.v) 4 | [DeBruijn](src/DeBruijn.v) 3 | [Combinators](src/Combinators.v) 3 | [InformationOrdering](src/
【文件预览】：
hstar-master
----.gitignore(220B)
----README.md(5KB)
----metrics.py(5KB)
----LICENSE(561B)
----install_coq.sh(297B)
----sandbox()
--------Nontermination.v(23B)
--------pcf.v(3KB)
--------GoedelsT.v(3KB)
--------DeBruijn.v(17B)
--------DirectedSets.v(8KB)
--------Compile.v(16B)
--------Unification.v(2KB)
--------ComprehensionNotation.v(2KB)
--------ObAxioms.v(8KB)
--------Constructor.v(4KB)
--------Lambda.v(6KB)
--------InformationOrdering.v(28B)
--------Codes.v(14B)
--------phoas.v(2KB)
--------unification.py(2KB)
--------confluence.v(1KB)
--------make.sh(123B)
--------Simple.v(4KB)
--------TypeInference.v(5KB)
--------Combinators.v(20B)
--------pretty.v(4KB)
--------Notations.v(18B)
--------Substitution.v(21B)
--------BohmTrees.v(18B)
--------Points.v(11KB)
--------Convergence.v(20B)
----src()
--------Nontermination.v(2KB)
--------StrongConstructor.v(6KB)
--------DeBruijn.v(11KB)
--------Compile.v(13KB)
--------TypeConstructor.v(14KB)
--------Annotate.v(17KB)
--------InformationOrdering.v(16KB)
--------Codes.v(16KB)
--------LeastFixedPoint.v(4KB)
--------make.sh(123B)
--------Combinators.v(8KB)
--------Notations.v(2KB)
--------Substitution.v(6KB)
--------BohmTrees.v(17KB)
--------Convergence.v(4KB)
--------Types.v(33KB)
----requirements.txt(23B)
----doc()
--------main.tex(2KB)
--------Makefile(613B)
--------references.bib(3KB)
----.travis.yml(515B)
----Makefile(457B)