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

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

ProofCafe

良く使うデータ型 †

数値 †

自然数型nat †

自然数型は代数データ型で帰納的に定義されている。

Inductive nat : Set :=
| O : nat
| S : nat -> nat

これは以下のような対応で自然数を表現している。

3とか12とかの数字リテラルや+,-,*,<,<=などの演算子をnat型として使うにはnat_scopeをOpen すればよい。(デフォルトでオープンされている)

Open Scope nat_scope.

整数型Z &dagger;

有理数型Q &dagger;

実数型R &dagger;

判定結果の型 &dagger;

bool &dagger;

sumbool &dagger;

組 &dagger;

pair &dagger;

文字、文字列 &dagger;

string &dagger;

ascii &dagger;

リスト構造 &dagger;

list &dagger;

Stream &dagger;

型の型 &dagger;

Set &dagger;

Prop &dagger;

Type &dagger;