No Such Blog or Diary

という言葉が一瞬通じなかった．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 って何やってるのよ？

assert → apply とかいうコンボを使いまくっていたら，specialize 使えよアホというコメントを貰った．確かにアホだ．

閑話休題．

Leibniz equality ではなく equivalence relation を使って物事を定式化しようとすると証明が色々ととても面倒．rewrite とかが動かないのが非常にストレスなわけで……　Equivalence relation 用の rewrite とかあったりするのか？　なければ自前で用意すりゃいいんだろうけどああ面倒．

土日乗り放題で 3.6ユーロ．通常１回1.4ユーロなので３回乗ったら元が取れる．30回の回数券だと35.2ユーロなので4回乗らないと元が取れんけど．

お出かけ＋買い物＋大学に行くというのを週末にするにはこっちのほうがお得．

閑話休題．

日曜日とそれ以外の日との時刻表の差が激しすぎる……　日曜だと始発が2時間半以上遅くなるとか信じられん．