No Such Blog or Diary

~/.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 メソッドが見つかりません」というコンパイルエラーを食らって悩んでいるという……

世の中は広い．

とりあえず，parser には無茶を要求しないというのが正しい姿勢であると理解した．

そして何か使われてない謎コンストラクタがあったけれどまあ放置でいいや．