2016-01-31から1日間の記事一覧
ちょっと複雑だったのでメモ. Coqで帰納的に命題を定義する. 例: 自然数nは自然数m未満である. Inductive It : nat -> nat -> Prop := | It1 : forall n:nat , (It (S O) (S n)) | It2 : forall n:nat m:nat , (It n m) -> (It (S n) (S m)). とする. このと…
ちょっと複雑だったのでメモ. Coqで帰納的に命題を定義する. 例: 自然数nは自然数m未満である. Inductive It : nat -> nat -> Prop := | It1 : forall n:nat , (It (S O) (S n)) | It2 : forall n:nat m:nat , (It n m) -> (It (S n) (S m)). とする. このと…