Coqリポジトリのtrunkを見ると、次の2つの機能が入っていることがわかります。 Universe Polymorphism Primitive Projection Universe Polymorphismは、グローバル定義をUniverseのレベルについて量化した形で定義することができる機能で、型に飾り付けをし…

Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。ここではその一部を取り上げて、意味を説明する。 前提知識 公理を仮定しない状態では、 Coqの論理は直観主義論理である。 ある2つが「等しい」という命題が証明で…

%COQ%\share\themes\MS-Windows\gtk-2.0\gtkrc を %COQ%\etc\gtk-2.0 の下にコピーする。ただし、%COQ%はCoqのインストールディレクトリのことを指すとする。たとえば %COQ% = C:\Program Files (x86)\Coq

目的 GCJなど一部のプログラミングコンテストでは既存のライブラリを使用することが認められている。特にC++であれば多倍長整数ライブラリとしてGMPを使うのが妥当であると考えられる。GMPを直接叩くのもよいが、GMPのC++バインディングを使うのが簡単である…

目的 PowerPC64アセンブリの演習のための環境を手元で構築する． 最新情報へのリンク 2015/01/11 以下のように事情が変化している。 PowerPC64 アセンブリ開発環境の設定メモに、以下の手順を現在行った場合に起きる問題への対処法がある。 crosstool-ngのバ…