- ゲームプログラムなら俺に聞け30
911 ：デフォルトの名無しさん[sage]：2015/01/21(水) 18:38:03.29 ID:OPHJ2hAi - ふっ？
|
- 集合論に基づいた言語を作りたい
841 ：片山博文MZ ◆T6xkBnTXz7B0 []：2015/01/21(水) 22:08:31.55 ID:OPHJ2hAi - >>840
Require Import Arith.
Theorem t: forall n:nat, 2*n = n+n.
intros.
replace (n+n) with (1*n + 1*n).
replace 2 with (1+1).
apply mult_plus_distr_r.
auto.
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
Qed.
|
- プログラミング雑談スレ ♯♯ [転載禁止]©2ch.net
63 ：片山博文MZ ◆T6xkBnTXz7B0 []：2015/01/21(水) 22:13:45.19 ID:OPHJ2hAi - お前のナイフが豚肉で汚れるだろ！
止めとけよ。
|
- プログラミング雑談スレ ♯♯ [転載禁止]©2ch.net
64 ：片山博文MZ ◆T6xkBnTXz7B0 [sage]：2015/01/21(水) 22:20:58.13 ID:OPHJ2hAi - 神聖なる領土を異教徒の血で汚すな
|