2007-08-01から1ヶ月間の記事一覧

ポジティブ型とマイポジティブ型

Require Import Print Inductive Definition Fixpoint Lemma Theorem Proof Qed intro intros induction unfold fold apply simpl rewrite reflexivity case discriminate trivial assumption

（＊＊ Remark 今回はZArithモジュールを使うよ。 Require Import ZArith. をタイプしてね。 ＊） 導入 Coqでは、整数全体の型はZで表され、次のように定義されている。 Coq Z | Zneg : positive -> Z Z0はゼロで、Zposは正の数、Znegは負の数を表している。…