12/03/09 10:17:33.18
O を起点として
O と (S O) だけの Typeとか
O と (S O) と (S (S O)) だけの Type とか
O と (S O) と (S (S O)) と (S (S (S O))) だけのTypeとか
...
を作りたかったのですが、そうするにはどういうコマンド入れたら良いのでしょうか>
レベル低い質問ですみません。
Inductive my : Type := O : my | S : my -> my.
こうしちゃうと O と (S O)だけじゃなく (S (S O))も myタイプになってしまうのでどうしたらよいのかわかりません。