对应于* _rect系列功能的合作原理

定义一个新类型foo给出了递归原则foo_rect，其优雅地摘要了fix。是否可以通过“翻转箭头”来定义一个合作的等效物（摘自cofix）？对应于* _rect系列功能的合作原理

2017-06-18 Carl Patenaude Poulin

希门尼斯和Castéran[执行]（http://www.labri.fr/perso/casteran/RecTutorial.pdf）“公园的原则” ，基本上是通常的归纳图式的镜像。在Adam Chlipala的*依赖类型认证编程*和Catalin Hritcu [已发表]（https：//hritcu.wordpress）中也有[http://adam.chlipala.net/cpdt/html/Coinductive.html] （1）（http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/HW6）（2012/12/23/learning-teaching-coinduction-with-coq /） .v），[2]（http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/HW67.v））。 –

这是不可能的，因为Coq检查cofixpoints的守卫条件的非模块化方式。幸运的是，Paco library只要您以特定的方式对您的定义进行短语说明，就可以完全按照您的要求来解决此问题。

这是一个很好的教程为帕科库在这里：在勒柯克http://plv.mpi-sws.org/paco/tutorial.html

来源

2017-06-22 19:38:37 Gregory

对应于* _rect系列功能的合作原理

回答

相关问题