文件名称：paco:一个用于参数化共生的Coq库
文件大小：150KB
文件格式：ZIP
更新时间：2024-06-06 23:21:58
Coq
Paco：用于参数共归的Coq库 Paco是用于参数化共生的Coq库。 有关更多信息，请参见： 钟基尔·胡尔（Georg Neis），德里克·德雷尔（Derek Dreyer）和维克多·瓦菲阿迪斯（Viktor Vafeiadis）。 。 POPL 2013。 Yannick Zakowski，Paul He，Chung-Kil Hur和Steve Zdancewic。 。 CPP 2020。 Paco还支持使用“伴侣”的最新技术。 看： 达米安·普斯（Damien Pous）。 。 LICS 2016。 Minki Cho重构了实现以加快编译时间。 当前版本是v4.1.1，并且与Coq 8.9-8.13兼容。 安装 # from opam opam repo add coq-released https://coq.inria.fr/opam/released opam
【文件预览】：
paco-master
----.travis.yml(883B)
----LICENSE(1KB)
----CHANGES(3KB)
----src()
--------paconotation_internal.v(9KB)
--------gpaco2.v(24KB)
--------paco_internal.v(4KB)
--------paco.v(138B)
--------gpaco11.v(27KB)
--------gpaco8.v(25KB)
--------gpaco7.v(25KB)
--------paco10.v(8KB)
--------gpacoall.v(501B)
--------paco9.v(8KB)
--------examples.v(9KB)
--------example_upto.v(3KB)
--------paco7.v(7KB)
--------gpaco12.v(28KB)
--------gpaco13.v(28KB)
--------paconotation.v(15KB)
--------gpaco4.v(24KB)
--------gpacotac.v(19KB)
--------paco13.v(10KB)
--------tutorial.v(24KB)
--------index.html(3KB)
--------paco4.v(6KB)
--------gpaco0.v(24KB)
--------paco12.v(9KB)
--------paco1.v(6KB)
--------paco5.v(6KB)
--------gpaco14.v(29KB)
--------gpaco3.v(24KB)
--------pacotac.v(6KB)
--------hpattern.v(4KB)
--------gpaco1.v(24KB)
--------gpaco10.v(27KB)
--------gpaco5.v(25KB)
--------paco11.v(9KB)
--------pacoall.v(486B)
--------paco0.v(5KB)
--------gpaco9.v(26KB)
--------.gitignore(53B)
--------paco3.v(6KB)
--------gpaco6.v(25KB)
--------Makefile(641B)
--------pacotac_internal.v(122KB)
--------paco6.v(7KB)
--------paco14.v(10KB)
--------paco2.v(6KB)
--------paco8.v(7KB)
--------main.css(822B)
----metasrc()
--------coq2py.sh(3KB)
--------paco_internal.v(4KB)
--------pacotac_internal.py(17KB)
--------gpacotac.py(5KB)
--------pacotac.py(4KB)
--------paconotation_internal.py(1KB)
--------pacolib.py(649B)
--------gpaco.py(39KB)
--------paco.py(11KB)
--------build.sh(875B)
--------paconotation.py(2KB)
--------build-add.sh(371B)
----.gitignore(100B)
----README.md(1KB)