TaPL、数学者がテキトーにやってる箇所がちゃんと全部書いてあったりするのかな……なんか、型環境とか……

依存型理論の中で依存型理論やるのやっぱり大変なんだ（数学者がやればできるでしょと言って怒られるやつだ）

Agda の "正しさ" がすごい

Maybe 型、理論屋さん感がすごくてよい

Agda の parameter と index の区別、フォーマルにはよくわかってない

∷ (U+2237) と ::（コロン (U+003A) 2 つ）の区別がつかずに詰まっていた

やっぱり Emacs に戻ろうかな……いまはもう Gemini 君いるから Emacs LISP もなんとかなりそうだし……

inductive type わからね～

実績解除：高輪ゲートウェイ駅に降り立つ

あと Gem というやつで「コーディングパートナー」というのがあって、こっちのほうがコーディングに強いのかなと思ってしばらく使ってたけど、なんかポンコツだな……と思ってやめたら、ふつうの Gemini のほうが賢かった