Coq
名前の管理が甘い、名前空間が粗末 ユニコードを考慮してない。アスキー偏重。 Mizar以外は、スクリプト言語またはそのシンタックスシュガー。 ブロック構造を意識してないか曖昧。 文書構造を意識してないか粗末 型クラスがあと付けで歪んでいたり問題を抱…
https://coq.inria.fr/library/Coq.Init.Notations.html より： Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x <-> y" (at level 95, no associativity). Reserved Notation "x ∧\ y" (at level 80…
C-c C-n しか憶えてない。http://proofcafe.org/wiki/ProofGeneral より： command action C-c C-n 1ステップ進む C-c C-u 1ステップ戻る C-c C-Enter カーソル位置まで進める C-c C-a C-o SearchPattern C-c C-a C-p Print C-c C-a C-c Check C-c C-a C-s S…
型クラスのパラメータ問題（トラブルっぽい話）が出てくるのは、指標とモデルの相対性の考察が不足しているせいだと思う。グロタンディーク平坦化を“積分”とみなしてのフビニに定理だと思う。繰り返し積分と同時多重積分の同値性。直積領域の積分ではなくて…
MLのモジュールシステムは禁欲的で、必要最小限の機能だけだが、スッキリしていて好きだ。だが： signatureにパラメータを付けられない。functorは当然にパラメータ（引数）を持つが、functorの値はstructureであってsignatureを値には取れない。 これは当然…
昨日の 型クラスの比較 - 檜山正幸のキマイラ飼育記 メモ編 への補足説明。既存のものに後からゴチャゴチャ文句を言うのは簡単だ。だから文句言う。コアージョン（coercion - 檜山正幸のキマイラ飼育記 メモ編）は必要悪という意味で必須だから、使うのはい…
Standard MLが圧倒的に良くできているな。オーバーロードを意図してない、型システムじゃない、という問題点はあるが、許せる、許せる。Haskellは「悪いお薬」をキメている。当座はとても元気が出るが、いずれは心身を蝕むアレ。型名に対するコアージョンを…
型ヒントという概念を導入する。型ヒントは Hint{name1: typeList1, ..., nameN: typeListN} という形。 型ヒントを使って、termの型を推論する。 ここのtermは、「レコードterm＝レコードインスタンス」であってよい。 型コンテキストは、型ヒントの特殊な…
Coqの物理的なモジュールの実体は.voファイル。コンパイルしたオブジェクトファイル。オブジェクトファイルの検索パスはロードバスと呼ばれる。表示は： Print LoadPath.
基本概念はレコード型とレコードインスタンスとレコードのアプライだけでなんとかなるのでは？ レコード型は、{name1 : type1; ..., nameN : typeN; } の形 レコードインスタンスは、{name1 := val1; ...; nameN := valN; } の形 未割り当て型宣言と値割り当…
構文 - 檜山正幸のキマイラ飼育記 メモ編に書いたが、クラス定義などで余分なセミコロンが書けないのは極悪だ。一般に、区切り記号を末尾で許さないのはいつでだって不快かつ不便。
過去に自分で書いた練習用のソースを読んでみる。 アットマークを多用しているが、これはなんだっけ？ Class定義で、波括弧ナシとアリでどう違う？ クラスパラメータで、中括弧はなんだ？ たしか自動的に補完するとかだったか。 アンダースコアは特殊な名前…
C-c C-n 次の行を解釈する（Next）。 C-c C-u ひとつ前の戻る（Undo） C-c C-j そこまで実行、または そこまでUndo。 Print ターム . タームの値と型を表示する。 Check ターム . タームの型を表示する。 About 名前 . その名前に関する情報を表示する。
しばらく触ってないとテキメンに忘れる。 Require ってどう使う？ Require Import/Exportって何？ Class定義構文、Class Foo : Bar のBarってどう使う？ Notationのスコープってどうやって使う？ スコープバインドは、Bind Scope hoge_scope with Hoge. みた…
Coqの構文について思うことをメモしていく。 letが1個の変数しか束縛できないことは意外と不便ではない。ブロック囲み記号（特にエンドマーカー）が不要なので入れ子が深くならない。単に代入文を並べている感じになる。 matchのケースの先頭に余分な '|' を…
Coqの型クラスについて思うことをメモしていく。 フィールド名が大域的なのは最低。フィールド名を局所化すれば出来る事が色々あるのに。ミクシンはその一例。 フィールドアクセッサの構文がない。f x の代わりに x.(f) が使えるようだが使いにくいし、そも…
