No Such Blog or Diary

普通に関数型言語として使うのは問題ないけれど依存型で変なことしようかなと思い始めるあたりでごちゃごちゃと……　Prop と bool の違いではまりまくるとか．どこに気をつけるべきなのかがはっきり見えないので修行あるのみ？

Coq 8.4 用のはバグってる？　生成される関数の本体であるラムダ式が型引数を通常の引数と同様に受け取ろうとしているような気が……　関数の型が合わないという文句を言われる．どうやら Haskell を吐いても Ocaml を吐いてもおかしいらしい．

とりあえず 8.3p12 用で我慢するか……　別の部分が 8.4 の機能を使っている気がしなくもないのだけど大丈夫かな？

つか，１日に２回も coq をコンパイルすることになるとは．

Coq を入れて proof general 入れてごにょごにょ．結構メンドイなぁ．証明の仕方がわかっても具体的に Coq をそのとおりに動かすのが慣れてないので手間かかる．うーん．

無事にお仕事その一は終了したが，お昼とかに周りの連中の会話を聞いていたのだけど全くフランス語がわからない．赤ん坊とかどうやって言語獲得してんだ？　とりあえず第二外国語はドイツ語だったし，フランス語とか基本の単語もわからない．出口が Sortie だとか駅が Gare だとか確定が Valider だとか程度の名詞がいくつか分かる程度の能力．

うーん，悲しいのでちょいとフランス語をお勉強しよう．

閑話休題．

時差ボケがまだ……

オルレアンへ移動した．RERのBが改装中につきシャルル・ド・ゴール国際空港から５駅ぐらいが使えないという罠にハマった以外は平和だった（バスで B のもう一方の端まで輸送中）．

さて，明日は仕事だ．寝るか．

ホテルの予約１日分間違ってたので面倒という罠．ま，いいか．

明日は早いので空港近くに移動．