メイドさんに教わったCoqというものをマニュアルと格闘しながら理解したつもり。 Variables A B : PropA と B は命題だよ。 Theorem mp : (A->B)->A->B. auto. Qed.modus ponens ぐらいは自動で証明できるよ。 Variable p : A->B. Variable a : A.なぜか知ら…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。