2010-07-04http://d.hatena.ne.jp/kururu_goedel/20100702 これを見て、とりあえず綺麗に書き直そうとしてみたら一日かかった。 しかし、これで一般たらいまわしへの道も見えてきたかも？ ここに置いた。http://github.com/kik/sandbox/blob/master/coq/tarai.v 多少、解説 Fixpoint ntarai3 (n : nat) (a b c : option Z) := match a with | None => None | Some av => match b with | None => None | Some bv => if Z_le_dec av bv then b else match n with | 0%nat => None | S np => match c with | None => None
