- 115 名前：デフォルトの名無しさん mailto:sage [2011/11/12(土) 12:39:28.72 ]
- >>114 nat以外のものも構造的帰納法を表しているだけ。
X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても
型だけわかれば、使えるからそれで いいと思う。
このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが
知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。
↑キャッシュ検索、類似スレ動作を修正しました、ご迷惑をお掛けしました |
Coqスレ
| |
read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef