近況報告
もうず〜っとElinっていうゲームやってて他のコトなんもできず、おろそかになり続けている。うごご。 実際久しぶりにこのブログどうなってるかなって見てみたらAIくんへのお布施が足らず、画面生成ができなくなってた。orz ってわけでお布施がたりなくなったら過去に生成した画面を適当に表示するようにしてみた。 Yeah. たぶんうごいてる...?面倒だからテストなんてちょろっとしかしてないけど、まあいいでしょ。
定理証明支援系
最近lean4をチョロチョロ書いたりなんだりしてるんだけど、やっぱり日本語命名ができないのがつらい。 coqはそれができるんだけど、vscode拡張機能が死んでてまともに補完とかがうごかない... なんかいい感じの定理証明支援系ないもんかなあ。