一日ごろごろしてました。 ほとんど成果ないですが、引っかかっているポイントが浮かび上がってきたので、メモしておきます。 Haskell 前回の畳み込みを使った表現がまだ解決していないCoq 4で割ると3余るならば真を返す関数が定義できないFixpoint is_4n_3 …