11/11/12 12:39:28.72
>>114 nat以外のものも構造的帰納法を表しているだけ。
X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても
型だけわかれば、使えるからそれで いいと思う。
このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが
知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。
11/11/12 12:39:28.72
>>114 nat以外のものも構造的帰納法を表しているだけ。
X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても
型だけわかれば、使えるからそれで いいと思う。
このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが
知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。