ProofCafe 第1回
ProofCafe 第一回でつぶやかれた内容です。おおまかな流れを実況したポストは、赤字にしてあります。
資料は、 http://coq.g.hatena.ne.jp/yoshihiro503/20100331 から辿れます。
-
- いいね！0
クラなんとか
@clairvy2
Mac 多し．できないことはないけど，まぁ，つぶやくという方向かと RT @r153: どえりゃーか、、流石に今日はust無い、、わな? #ProofCafe
2010-04-25 14:15:49
Keigo Imai
@keigoi
Gallina は 型も式である。 型の型は Set である。 だから たとえば「『nat型』の型」を調べる (Check nat.) と、 Set が返ってくる。 #ProofCafe
2010-04-25 14:21:21
Keigo Imai
@keigoi
ほかに 命題の型 Prop というのがある。 Check 1=2. と入力してみよう。 型 Propが返ってくる。 #ProofCafe
2010-04-25 14:24:14
Keigo Imai
@keigoi
式を識別子に束縛するにはコマンドDefinition を使う。 識別子の名前は小文字でも大文字でもよい。 Gallina は 型も値と同様に扱えるので Definition t := list nat . のように型をDeifnitionで識別子に束縛できる #ProofCafe
2010-04-25 14:25:49
Keigo Imai
@keigoi
Inductive コマンドで 型を定義する。 ここで Joker や Heart などはコンストラクタ #ProofCafe
2010-04-25 14:26:39
Keigo Imai
@keigoi
Fixpoint は再起関数を定義する。 Definition との違いは、 定義本体で再起呼び出しができること。 #ProofCafe
2010-04-25 14:28:13
でこれき
@dico_leque
Inductive は「帰納的」という意味。自然数のリストとかは Inductive nList : Set := | Nil : nList | Cons : nat -> nList -> nList. と帰納的なデータ構造 #ProofCafe
2010-04-25 14:28:40
Keigo Imai
@keigoi
Coq では、自然数は O (オー;ゼロの意味) と S n (n+1の意味)で表現する。 1, 2, 3.. などと書くと、自動的に S (S (S O)) などと 展開される。 #ProofCafe
2010-04-25 14:29:46