Coqで圏論の会

ω･`)にべべb @2bbb

何一つ分からない. #concat

ω･`)にべべb @2bbb

取り敢えず今朝osxにpkg使ってCoqIDE入れた環境にConCaT入れたときの話でも. #concat

ω･`)にべべb @2bbb

いや, 単純にパスに /Applications/CoqIdE_8.3.app/Contents/Resources/bin 通してmakeとmake installしてCoqIDEのパッケージ開いてuser-contribにConCaTをコピー. #concat

ω･`)にべべb @2bbb

まあ, pkg使ってインストールしてるような軟派な人は居なさそうだけど. #concat

ω･`)にべべb @2bbb

:> ってどういう意味か教えて偉い人 #concat

ω･`)にべべb @2bbb

"Structure > Map" の > の意味も分からない. 教えて偉い人. #concat

ω･`)にべべb @2bbb

何が分からないって構文が分からない. 何が分からないって英語が分からない. 仕方無いので本でも読もう.

ω･`)にべべb @2bbb

:> って評価順の問題とかだったりすんの？

Takashi Miyamoto @tmiya_

Coq で圏論、のイベントに参加中。#concat

ω･`)にべべb @2bbb

でも Ob :> Type の意味とか分からんなぁ. 煙草吸いに行こ.

ω･`)にべべb @2bbb

しかし, Check x :>. とかしてもxが表示されるだけだしなぁ.

ω･`)にべべb @2bbb

Structureの中で出て来るときは関数型以外に使うと怒られる. うーん. 煙草煙草.

Takashi Miyamoto @tmiya_

@2bbb 私もあまり :> は判ってないのですが、coercion 出来る、みたいな感じ。a:A は a は A 型、a :> A だと a は A に変換出来る、みたいなものかと。というか @kikx さんか @pirapira さんに聞くべきかな。#concat

ω･`)にべべb @2bbb

@tmiya_ うーん... 分かったような分からない様な... もうちょい調べてみます. ありがとうございます.

ω･`)にべべb @2bbb

よし, ConCaT読むのは諦めた.

[1..100]＞＞=pen @1to100pen

ConCat のページから wget -r してるがまだ終わらない。 (;_;)

Masahiro Sakai @masahiro_sakai

とりあえず、Category.vをCoqIDEで読んだ。型理論で圏を定義するよくあるやり方だけど、Coqのテクニック的な部分が、僕のような初心者には難しい。 #concat

Masahiro Sakai @masahiro_sakai

お次はDual.vを読む。 #concat

Masahiro Sakai @masahiro_sakai

む。この Build_Category というのは、どこで定義されてるんだ？ #concat

Masahiro Sakai @masahiro_sakai

Build_Category は Structure Category : Type := 〜. で定義されてるみたいだが、Build_Category is defined みたいなメッセージは出て来てなかった…… #concat

Masahiro Sakai @masahiro_sakai

PCがネットにつながってないと、マニュアルが見れなくてつらい。事前にダウンロードしておくべきだった。 #concat

Sosuke MORIGUCHI @chiguri

@masahiro_sakai type classの定義でも同様の関数が作られますが、メッセージは出ませんね。Structureは使ったことがないのでちょっとわかりませんが。

Masahiro Sakai @masahiro_sakai

oの引数の順番が、普通と違うっぽい。これは酷い。順番変えるなら、別の演算子にして欲しい…… #concat

シャミノ @syamino

#concat　Coqさっぱりわからない状態で来てしまったのでチュートリアル写経しかできてないなー

Masahiro Sakai @masahiro_sakai

iPhoneのGoodReaderで落としたリファレンスマニュアルをiTunes経由でPCに転送。これで勝つる。 #concat