Logical Foundationsを進めがてら、基礎固め的に簡単な命題論理の命題を証明してみたいと思ってググったらこんなスレに遭遇した： coq.discourse.group このうちの最初の問題が簡単ながらもいくつか面白い点があったのでメモ。 証明する命題： Lemma a1 : fo…

Coqでソフトウェア工学の基礎をいろいろ証明するよという趣旨（多分？）のSoftware Foundationsというウェブ上で読める教科書シリーズがある。 softwarefoundations.cis.upenn.edu 第1巻Logical FoundationsはそのままCoqの教科書になっている。これを読み進…

四月はCoqとClojureをやっていきたい— zehnpaard (@zehnpaard) March 27, 2021 というわけでemacsでcoq環境を整備したのでメモ。 インストールが必要だったもの： coq proof general spacemacs-coq 前提として spacemacs opam は入っているものとする（opam…