作ってみた - 菊やんの雑記帳http://as305.dyndns.org/aps/ サブミットのしかた。 DefinitionsがあるときはDefinitions.vに保存してコンパイル TheoremをTheorems.vに保存。Proof.〜Admitted.の間を埋めて証明できたら、Admitted. をQed. にしてファイルを送信 問題の作成 http://as305.dyndns.org/aps/problem_checker.tgz をダウンロード。exampleと同様にDefinisions.v, Theorem.v, Verify.v を作成。 check を実行して、成功したら各ファイルを送信。公理を足したいときは、checkの出力の最後の部分を少し編集して、Assumptionのとこに書く。
anarchy proof -
