Coqでの証明はtacticと呼ばれるコマンドを並べて次々に実行ことによって行われる。 このtacticの語彙が多いほど証明の記述は楽になる。 しかし、語彙を増やすようなドキュメントはオンラインに見つからないので、書きやすいところから書いてみる。 exact ter…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。