Skip to content

Instantly share code, notes, and snippets.

@srbmiy srbmiy/ssrnat001.v
Created Dec 20, 2014

Embed
What would you like to do?
Require Import ssreflect ssrbool ssrnat.
Definition nand_b (b0 : bool) (b1 : bool) : bool :=
match b0 with
| true => (~~ b1)
| false => true
end.
Lemma nand_lemma : forall (b0 b1 : bool), (nand_b b0 b1) = (~~(b0 && b1)).
Proof.
move=> b0 b1.
case b0.
simpl; reflexivity.
simpl; reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.