2013-04-11から1日間の記事一覧
例えば # REAL_NEG_MINUS1;; val it : thm = |- !x. --x = -- &1 * x を `-- x` に適用しようと # REWRITE_CONV [REAL_NEG_MINUS1] `-- x`;; としても...帰ってきません.これは等式の右辺の -- &1 にも同じ書き換えが適用され,ループに陥っている為です…
例えば # REAL_NEG_MINUS1;; val it : thm = |- !x. --x = -- &1 * x を `-- x` に適用しようと # REWRITE_CONV [REAL_NEG_MINUS1] `-- x`;; としても...帰ってきません.これは等式の右辺の -- &1 にも同じ書き換えが適用され,ループに陥っている為です…