関数型プログラミングで実用的なプログラム書ける人すごそう、頭こんがらがりそう

確かに、Agda は標準ライブラリの大小関係の定義からしてもう Curry–Howard 前提なんだ

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

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

Agda の "正しさ" がすごい

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

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

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

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

inductive type わからね～