ProofCafe/Coq02 のバックアップソース(No.1)

• バックアップ一覧
• バックアップ を表示
• ProofCafe/Coq02 は削除されています。
  • 1 (2010-04-06 (火) 01:05:19)
  • 2 (2010-04-06 (火) 13:51:15)

[[ProofCafe]]

*良く使うデータ型 [#k230eb54]
**数値 [#db5b3131]
***自然数型nat [#nbb6b557]
自然数型は代数データ型で帰納的に定義されている。
 Inductive nat : Set :=
 | O : nat
 | S : nat -> nat
これは以下のような対応で自然数を表現している。
|0| O|
|1| S O|
|2|S (S O)|
|3|S (S (S O))|
|...|...|
|12|S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))|
|...|...|

3とか12とかの数字リテラルや+,-,*,<,<=などの演算子をnat型として使うにはnat_scopeをOpen すればよい。(デフォルトでオープンされている)
 Open Scope nat_scope.
***整数型Z [#e2f45a2d]
***有理数型Q [#j5cc7152]
***実数型R [#b8976e02]

**判定結果の型 [#i78f79ed]
***bool [#if65958a]
***sumbool [#v2b556b4]

**組 [#p7b4a5c3]
***pair [#qeb46f2d]

**文字、文字列 [#mf9a3992]
***string [#if786eac]
***ascii [#gf65dbf8]

**リスト構造 [#f5e08c70]
***list [#pf2afb9a]
***Stream [#l80116e2]

**型の型 [#h458219a]
***Set [#x80ac075]
***Prop [#t07da4ee]
***Type [#n8156201]