「coq入門」の入門

ssreflect初心者coqideCoq新人プログラマ応援Coq
SVG

第33回 #ProofCafe での練習問題のssreflectを使った解答例。

ProofCafeCoqProofGeneralssreflectCoq
SVG

Equiv_Jの練習問題 WHILE_true

SoftwarefoundationsProofCafeCoqssreflectCoq
SVG

ssreflect tutorial(意訳版) [作業中]

CoqssreflectCoq
SVG

Equiv_Jの練習問題assign_equivの証明 #ProofCafe

SoftwarefoundationsProofCafeCoqssreflectCoq
SVG

Ssreflect Tutorial最初のコード

CoqssreflectCoq
SVG

リフレクションを使って集合の問題を解いてみる

証明CoqssreflectCoq
SVG

SSReflectによる鳩の巣原理の証明

証明CoqssreflectCoq
SVG

AffeldtさんのSsreflect練習問題exo4

ProofCafeCoqssreflectCoq
SVG

AffeldtさんのSsreflectチュートリアルのソースをビルドする

AffeldtProofCafeCoqssreflectCoq
SVG

MathComp で文字列を使う

CoqssreflectMathCompCoq
SVG

有限集合の濃度の存在を証明する

証明CoqssreflectMathCompCoq
SVG

MathComp における古典論理

証明CoqssreflectMathCompCoq
SVG

Coq/SSReflectでたった1行のコマンドで完全帰納法を適用する方法

Coq完全帰納法ssreflectCoq
SVG

Coq/SSReflect/MathCompの文献

CoqssreflectMathCompCoq
SVG