定义一个新类型foo给了我一个递归原则foo_rect，它优雅地抽象了过来fix。cofix是否可以通过某种方式“翻转箭头”来定义同义等价物（抽象）？
问问题
140 次
1 回答
2
由于 Coq 检查 cofixpoints 的保护条件的非模块化方式，这是不可能的。幸运的是，Paco 库通过完全按照您的要求来解决这个问题，只要您以特定的方式表达您的定义。
这里有一个很好的 Paco 库教程：http: //plv.mpi-sws.org/paco/tutorial.html
于 2017-06-22T19:38:37.693 回答