zero-based でないことで顰蹙を買いまくっている音楽の度数
仕様 (specification) があるならなんでも依存型理論で書けるっしょみたいな精神なのかな……
「音楽理論は Agda のプログラミングをする中で勉強した程度なので……」←！？！？
音楽の話が始まった
関数型プログラミングで実用的なプログラム書ける人すごそう、頭こんがらがりそう
確かに、Agda は標準ライブラリの大小関係の定義からしてもう Curry–Howard 前提なんだ
TaPL、数学者がテキトーにやってる箇所がちゃんと全部書いてあったりするのかな……なんか、型環境とか……
依存型理論の中で依存型理論やるのやっぱり大変なんだ（数学者がやればできるでしょと言って怒られるやつだ）
Agda の "正しさ" がすごい
Maybe 型、理論屋さん感がすごくてよい
