作ってみた
サブミットのしかた。
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のとこに書く。