■

オンライン演習も終ったし、仕事がヒマな内に、Coqに戻るかと思ったけど、やはりもう色々忘れてていろいろいやになる。年とるのってやだねえ。しかし若いころは経験と理解力と忍耐力が足らんかったから余り変わってないかもしれん。

Software Foundation
Basics.vにて、
関数定義が減少的でなくてはならない。ということで、

Fixpoint div (n m :nat) :nat :=
 match n, m with
 | O, _ => O
 | _, O => O
 | _, _ => S (div (minus n m) m)
end.

こんなんが駄目と。