2013-09-05から1日間の記事一覧
Coq modeで C-c C-f Find theorems containing: とミニバッファに出るので、定理を探したい型とか名前の一部とか入れると検索してくれる。Coqはまだ面白いけど、非形式証明になるとさっぱりお手上げ。 数学苦手。nとn'が同時に出てこられると混乱するんです…
Coq modeで C-c C-f Find theorems containing: とミニバッファに出るので、定理を探したい型とか名前の一部とか入れると検索してくれる。Coqはまだ面白いけど、非形式証明になるとさっぱりお手上げ。 数学苦手。nとn'が同時に出てこられると混乱するんです…