旧聞になりますが「大学生の４人に１人「平均」分からず 数学基本調査、論理力欠如明確に」より引用。 「偶数に奇数を足すと必ず奇数になる」ことを数式と文章で説明する中２レベルの問題 ということらしいので coq を使って自分が中二レベルあることを証明…

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