http://d.hatena.ne.jp/propella/20090215/p1 Coq < Parameter a b :nat. a is assumed b is assumed Coq < Print plus. plus = fix plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus p m) end : nat -> nat -> nat Argument s…

SF Induction.v #coqnormalizeにて、Prove It. とだけ書いてあるんですが、何を証明すればよいのでしょうか。これ？ 取り敢えず、normalizeする前の二進数とした後の二進数で、同じ自然数に変換出来ることは証明したけど、 これって意味あるんだろうか？そも…