No Such Blog or Diary

兎にも角にもめんどくさすぎてやってられん．つーか typeclass でライブラリ全部書き直されないかなぁ．

閑話休題．

モジュールの読み込みとインスタンス宣言のタイミングとの兼ね合いで個々の機能は動くのに合成した機能が働かない．いまひとつモジュールを絡めたスコープの扱いがよくわかってないな．要修行．

そして今日も無限ループと戦う．

Typeclass の eauto の深さ指定ができない．Typeclasses eauto := debug bfs 10 とかかくと 10 のところはピリオドだろと怒られる．うーん，書き方が悪いのか廃れたオプションがマニュアルにあるのか実装してないのにマニュアルにあるのか……

とりあえず，よくわからんけど無限ループしまくるのをどうにかして欲しい．デバッグも大変．すんごく微妙にインスタンスの優先度を設定したら無限ループを回避できたけど，もうちょっと頭良く探索してくれないかなぁ．

つか，dfs と bfs の切り替えもできてないような？

という言葉が一瞬通じなかった．Daylight saving time でオッケーだったと．

Wikipedia の Daylight saving time を見たらアメリカ英語的には daylight saving time なのね．"summer time" って言い方はイギリス英語であると．まあ，Daylight saving time より summer time の方が単純な単語を使っているから日本だとサマータイムってなるのかね．

閑話休題．

つまり月末の土曜の深夜で終わりなんだな．前回来た時とは逆向きの調整になるのか……　一日が２５時間になるはずだけどどの時間帯が重複するんだろう？

ディナーに連れて行ってもらったものの予約なしで適当に行こうぜ的なノリだったので当初の目的地には満員で入れず，適当に歩いて見つけた日本食レストランに面白そうだからと入ってみた．「ひかり」というお店で，この前行った Lift とかのある川の近くのレストラン街の一角にあった．１２，３年くらいやってるらしい．

感想：全くがっかりしないちゃんとした日本の料理だった．揚げだし豆腐がとても美味しゅうございました．天ぷらも美味しかった（寿司は食べてないので分からない）．

んで，日本の料理がフランスの作法に則って前菜から順に出てくるのは斬新だった．味噌汁もスープとして単品で出てきたし，普通のお椀（汁椀）に入ってぽつんと置かれるのでとても違和感があって面白い．何やらご飯とかとまとめて出すとフランスの人たちが困るとかでそうなっているそうな．ここらへんは習慣の違いよね．

今回は試せなかったのだけど，１日前に予約しておくとすき焼きとかもあるらしい．いなり寿司とか太巻きとかもその部類．機会があればここらを試してみたい気分．

ちなみに，女将さんは日本の方で日本語通じた．ウェイトレスさんは日本語ダメらしい．主人はちょっと日本語わかるらしい．

とりあえず，大当たりでしたとさ．久々に日本の料理が食べられて良かった．

まあ，exists x とか書かれていたとして具体的にどれが出てくるかとか証明上は関係ないのだから何かを取り出そうとしないというのが自然な思考なのだけど，ときどき値が取り出せたらなぁと思わなくない．

とりあえず Prop の扱いにまだ慣れていないらしい．

閑話休題．

証明を対話的にやるのが面倒だから直接プログラム書いてしまえと思うようになってきた．が，まだ tactic と実際のコードとの対応とかが把握しきれていないのでなんとも難しい．

パンだと少なすぎる気がする．半分以上空気じゃん．ご飯が恋しい．

閑話休題．

Function で定義した関数は Qed で終わらず Defined で終わっておかないと Eval compute とかで試しに動かした時にとても残念なコトになると学習した．ここらはもう少し中のことを理解しないとダメなんだろうなぁ……　つか，Function って何やってるのよ？