McCarthy の91関数を Coq で定義しようとすると，簡単にはできないことがわかります．具体的には， structural な recursion になっていない． measure がわかったとしても，nested な recursion は Fixpoint や Function で扱えない． こんなときは以前も話…

11ヶ月ぶりの更新です．Anarchy Proof に手を出してみました．Project Euler と違って，問題の定義が Coq の形式で与えられているので非常に楽です． # 当たり前方針としては，ゴルフは全くせずに他人が読んでもわかる(かもしれない)書き方をするつもりです…