2012-03-18から1日間の記事一覧
Coq.Sets.Ensembles がなんだかうまく使えないなあ,と思った話。ちなみに以下で使う諸定義は http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html を必要に応じて参照してください。具体的には何かというと, Coq < Goal forall x : A, forall X : Ensembl…
Coq.Sets.Ensembles がなんだかうまく使えないなあ,と思った話。ちなみに以下で使う諸定義は http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html を必要に応じて参照してください。具体的には何かというと, Coq < Goal forall x : A, forall X : Ensembl…