No Such Blog or Diary

およそ先月分の電気代だと思うのだけど，例年より高くて 1万円台だった．これまでこの時期は高くても 8千円だったのに……　今年はなぜか高い．

んで，何に電気食ってるんだろうと思ってしばらく考えてみた結果として，単純に今年は在宅勤務が入ってきて例年より自宅で暖房器具やら PC やらを使ってる時間が長いってだけだろうという結論に達した．去年から増えたりした家電も特に無いので．

ということで，通勤費の支出は減るけどそれ以上に電気代が増えるっぽいことに気づいた今日このごろ．夏場は以前から冷房24時間運転だったので冬ほどは差がなかったのだと思う．

~/.ssh/config を新しいノートPC に持ってってなかった……　滅多に書かないし書くとしても上のエントリをコピーとかなのでゼロからその場で書くのも無理．今日は面倒だった．

Xサーバも入れ忘れてた……　WSL から X なアプリを動かすことは少ないので需要が生じるまで忘れてる．今日はデモれなかった．

そういや WSL の中の Linux をまとめて持ってくるとかはできるのかな？　色々と忘れ物がありそうなのでガサッといけると楽なのだけど．

今日は朝から夜までずっと Coq と Ltac を相手に戦っていた．とりあえず，マジで目が疲れてるのか涙出る．

だがしかし，Ltac の動きがまだ把握しきれてない．特に Ltac の世界と Gallina の世界の切れ目がよく把握できてないので，変数名だと思ってるところを書き換えただけで想定通りに動いてくれなくなったりしてた．まだまだ修行が足りん．

そういえば Ltac2 は使いやすいのだろうか？　そのうち試してみよう．

Sony が α1 を出すそうで．α7 の上位に α9 が来て終わりかと思ってたので，「α1」って入ったタイトルのメールを見たときにはホテルの宣伝かなと一瞬思った．

だがしかし，高い．80万．素人の使うものではないな．

数学の本がいくらか行方不明．ほしいときに見つからない．どこに置いてたか……

なんとなく半年とか 1年とか前にも同じことを思ったような．新しく買ってしまったほうがはやいかも．

「加算のクラスは実装してあるから同様にして減算とか追加してね」という課題に対して，「"add" と入ってるコード部分を複製して "add" を "sub" に置き換える」という手法で作られたコードがやってきた．元コードの中でリストに要素を追加するために add メソッドを使ってる部分があるのだけど，そこも sub にされてて「リストに対する sub メソッドが見つかりません」というコンパイルエラーを食らって悩んでいるという……

世の中は広い．