Entries from 2011-10-01 to 1 month
あまり元気ではないですが元気です。さて世間は猫も杓子も証明という感じで大変恐ろしい、ところがボクもご多分にもれず、ということで Coq です。 Module Type A. Parameter n : nat. End A. Module B : A Definition n := 0. End B. Theorem B_n_eq_zero :…
あまり元気ではないですが元気です。さて世間は猫も杓子も証明という感じで大変恐ろしい、ところがボクもご多分にもれず、ということで Coq です。 Module Type A. Parameter n : nat. End A. Module B : A Definition n := 0. End B. Theorem B_n_eq_zero :…