自己紹介: 名前: デンシナ, 趣味: キーボード論理配列の変更, 好きな食べ物: 寿司, ラーメン, とんかつ, 焼肉, いつもいるところ: Misskey
日時: 2024/11/18
もうず〜っとElinっていうゲームやってて他のコトなんもできず、おろそかになり続けている。うごご。 実際久しぶりにこのブログどうなってるかなって見てみたらAIくんへのお布施が足らず、画面生成ができなくなってた。orz ってわけでお布施がたりなくなったら過去に生成した画面を適当に表示するようにしてみた。 Yeah. たぶんうごいてる...?面倒だからテストなんてちょろっとしかしてないけど、まあいいでしょ。
最近lean4をチョロチョロ書いたりなんだりしてるんだけど、やっぱり日本語命名ができないのがつらい。 coqはそれができるんだけど、vscode拡張機能が死んでてまともに補完とかがうごかない... なんかいい感じの定理証明支援系ないもんかなあ。