トップエスイーチュートリアル「Coqで学ぶ定理証明入門」

今日はセミナーを聞いてコック見習いを目指します #topse_coq

2011-07-12 10:07:22

rkyymmt @rkyymmt

参加者はHaskellerが多いようだ #topse_coq

2011-07-12 10:11:18

#topse_coq agda2も詳しく知りたい。というかまとまったチュートリアル(のも少し完成した版)がほしい...

2011-07-12 10:18:21

プログラミング言語としてみたとき#coq はTuring完全ではない。プログラミング言語をうたっている #agda は？ #topse_coq

2011-07-12 10:21:36

Mac 版のCoqIdE 上で Extraction すると，ルート直下にファイルができるのか #topse_coq

2011-07-12 11:21:14

あ〜，ルート直下ですか．同じように探してました．ありがとうございます:-) RT @tyasunao: Mac 版のCoqIdE 上で Extraction すると，ルート直下にファイルができるのか #topse_coq

2011-07-12 11:23:53

Mac 版の CoqIde のフォントを大きくした．Preference を開こうとすると落ちるので，Proof General なるものを入れて Emacs でやれるように挑戦してみよう #topse_coq

2011-07-12 11:40:10

"/Users/..." みたいにフルパスで書かないと駄目なんですね RT @koji8y: あ〜，ルート直下ですか．同じように探してました．ありがとうございます:-) ... #topse_coq

2011-07-12 11:41:37

inductiveなデータ型を作る．#topse_coq いつか #agda の依存型もきちんと使えるようになりたい．

2011-07-12 11:50:29

Carbon Emacs じゃバージョンが 22 だから ProofGeneral が入らないからだめじゃん．しょうがないので，Cocoa Emacs をダウンロードしてみるか．#topse_coq

2011-07-12 11:56:17

昼休みにシンクライアントのふた閉じて出て、戻ってきたら初期化されててあせった　#topse_coq

2011-07-12 13:02:33

#topse_coq proof-editing モードで何を成し得ているか．ひとつの正念場．

2011-07-12 14:14:04

#topse_coq #coq 証明した結果を証明木で表示したい．

2011-07-12 14:17:22

ようやく Cocoa Emacs がダウンロードできた．b-mobile だとつらかった．これで，ProofGeneral がコンパイルできるはずだ #topse_coq

2011-07-12 15:16:57

Yoshihiro Imai @yoshihiro503

x + 1 = S x という定理は無いけれど、x + y = y + x という定理を使えばx+1は1+xにできます。 #topse_coq

2011-07-12 16:06:51

Keigo Imai @keigoi

.@yoshihiro503 plus_n_Sm: forall n m : nat, S (n + m) = n + S m を使ってrewrite <- plus_n_Sm. とするのもアリ？ #topse_coq

2011-07-12 16:10:53

今日のセミナーで Coq がどういうものかの雰囲気は掴めたので，よかった．IS の単調性とかこういうので調べるようにしないといけないな．．．#topse_coq

2011-07-12 17:05:51

#topse_coq 告白しよう、最後まで「intro」が何の略なのかわからなかった

2011-07-12 17:16:45

@yoshihiro503 講師お疲れ様でした。Coq 初心者でしたが、どんなものかよくわかりました。#topse_coq

2011-07-12 19:00:20

introduction、仮説(hypotgesis)の導入? そういう意味でも初学者向けに、対応する証明木を示すのって有効(しつこいですね) RT @tobo: #topse_coq 告白しよう、最後まで「intro」が何の略なのかわからなかった

2011-07-12 22:20:55

ogawa kiyoshi @kaizen_nagoya

7/12 トップエスイーチュートリアル Coqで学ぶ定理証明入門　受講記録(1) http://t.co/CsBMf9p #topse_coq

2011-07-13 06:59:00