2016-01-13から1日間の記事一覧
Coqの帰納法を忘れかけてたのでメモ (** **** Exercise: 2 stars (false_beq_nat) *) Theorem false_beq_nat : forall n m : nat, n <> m -> beq_nat n m = false. Proof. intros n. unfold not. induction n as [ | n']. - intros m H (**ここでmをintros**…
Coqの帰納法を忘れかけてたのでメモ (** **** Exercise: 2 stars (false_beq_nat) *) Theorem false_beq_nat : forall n m : nat, n <> m -> beq_nat n m = false. Proof. intros n. unfold not. induction n as [ | n']. - intros m H (**ここでmをintros**…