* _rectの一連の関数に対応する誘導原理

fooの新しい型を定義すると、foo_rectという再帰の原理が得られます。この再帰の原理は、fixを基にしています。どのようにして「矢印を反転させる」ことによって、コインシデンス相当物（cofixで要約）を定義できますか？* _rectの一連の関数に対応する誘導原理

出典

2017-06-18 Carl Patenaude Poulin

ヒメネスとCastéran[実装]（http://www.labri.fr/perso/casteran/RecTutorial.pdf）「公園の原理」Coqの中には、本質的には、通常の誘導スキーマの鏡像である。 Adam Chlipalaの* Dependent Types *による認定プログラム*、Catalin Hritcu（published）（https：//hritcu.wordpress）の[議論]（http://adam.chlipala.net/cpdt/html/Coinductive.html）（[1]（http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/HW6）の問題集には、[.com/2012/12/23/learning-teaching-coinduction-with-coq/.v）、[2]（http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/HW67.v））。 –

これは、Coqがcofixpointの保護条件をチェックする非モジュール方式のため不可能です。幸いにも、Paco libraryは、特定の方法で定義をフレーズする限り、あなたが望むものを正確に行うことでこの問題を解決します。

ここでパコ・ライブラリーの良いチュートリアルがあります：http://plv.mpi-sws.org/paco/tutorial.html

出典

2017-06-22 19:38:37 Gregory

* _rectの一連の関数に対応する誘導原理

答えて

関連する問題