作ってみた

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のとこに書く。