2017-04-03から1日間の記事一覧
最近書いてるCoqの話。 主にこれの解説をします: Yoneda.v · GitHub Setoidをベースにすることについて 多分圏論formalize業界(狭そう)では有名な話。 Coqの場合はSetoidのequalityに対してもrewrite tacticが使えるのでそれでやる。 Proper Setoid morphism…
Coq 8.6をインストールしたときのあれこれ Coqのインストール Coq/SSReflect/MathCompの設定 これの通りにやるだけ aptのパッケージは古いからだめってあったので言われたとおりにopamでいれた それと~/.opam/4.04.0/binにパスを通すのもやった. どうもopam…