限量子の使いようが、いまひとつ理解しきれていない。 Isabelle の集合の条件部に EX を書くと、 EX の条件を満たすものが列挙される。 lemma "{0, 1, 2, 3, 4} = {u::nat. EX j k. j <= k & k < 3 & u = j + k}" apply auto apply (rule_tac x=0 in exI) ap…

PuTTY を使っていて、外部サーバーへの接続方法が ext-server (のような) 名前で保存されているとする。 > pscp -load "ext-server" <localfile name> <ext-server-account>@<ext-server name>:.</ext-server></ext-server-account></localfile>

正月休みにも継続できるよう、 Sourceforge のシェルアカウント内に Isabelle 環境を構築。公式のインストール手順に書かれている tarball を四つ落としてくる。 $ wget http://isabelle.in.tum.de/dist/Isabelle2008.tar.gz $ wget http://isabelle.in.tum.…

とあるクラスに int と double のキャストオペレーターが定義されている。このためユニットテストフレームワークが生成する operatorコンパイルできず困る、という話を伝え聞いた。そんなときは operatorオーバーロードを定義すればいいんじゃない？ #includ…

「は」と「が」。 「は」は文の切り離し、「が」は文の接着をする。「は」は問題を設定し、後にその答えを設定する -- 花は桜。 「は」は対比をつくる -- 私は猫は嫌い。 「は」は限度をあらわす -- 百万円にはならない。 「は」は再審をおこなう -- 美しく…

IE の失効リスト確認にかかわるエラーメッセージについて。 Security certificates are issued for a particular time period. But they can be revoked at any time. The fact that they have been, and why, is supposed to be available to applications.…

なんとなく訳してみた。 A remote code execution vulnerability exists as an invalid pointer reference in the data binding function of Internet Explorer. When data binding is enabled (which is the default state), it is possible under certain …

17.4.3.1 Reserved names [lib.reserved.names] の 17.4.3.1.2 Global names [lib.global.names]: Certain sets of names and function signatures are always reserved to the implementation: Each name that contains a double underscore (__) or begins…