文件名称：MPCTT:计算类型理论的建模与证明
文件大小：74KB
文件格式：ZIP
更新时间：2024-05-07 13:42:16
Coq
MPCTT教科书项目 使用Coq证明助手在计算类型理论中进行建模和证明（作者Gert Smolka） 随附的Coq文件在。 文本位于 。
【文件预览】：
MPCTT-main
----coq()
--------bsat.v(17KB)
--------fin.v(19KB)
--------regexp.v(7KB)
--------pat.v(6KB)
--------compiler.v(2KB)
--------vector.v(8KB)
--------lw.v(5KB)
--------bctt.v(3KB)
--------elim.v(3KB)
--------nat_lia.v(3KB)
--------post.v(863B)
--------ewo.v(5KB)
--------sizerec.v(4KB)
--------exquant.v(3KB)
--------infty.v(6KB)
--------ids_less.v(6KB)
--------pairing.v(1KB)
--------sdec.v(6KB)
--------ars.v(5KB)
--------ext.v(1KB)
--------crer.v(726B)
--------provability.v(3KB)
--------nat.v(6KB)
--------indeq.v(6KB)
--------leibniz.v(3KB)
--------gs.v(8KB)
--------list.v(18KB)
--------ids_gcd.v(2KB)
--------dat.v(18KB)
--------wfrec.v(12KB)
--------numeral.v(8KB)
--------gcd.v(13KB)
--------dec.v(1KB)
--------README.md(2KB)
--------nd.v(15KB)
--------xm.v(6KB)
--------aczel.v(4KB)
----README.md(246B)