Abort

Coqで定理を書いてみる

Coqは証明支援系 (Proof Assistant) と呼ばれるシステムで、定理などの証明を構築することができる。 今回はTheoremというCoqコマンドを使ってみる。 このコマンドを使って定理を記述し、宣言することができる。 文法 [Theorem 定理の名前 : 定理の内容.] 最…