對應於* _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系列功能的合作原理

回答

相關問題