max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/data/bool/lemmas): add (coe tt) and (coe ff) simp lemmas

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-05 09:50:01 -08:00
parent ddfdca2e57
commit 76f989d51c
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/data/bool/lemmas.lean
View file

@ -88,3 +88,9 @@ by cases a; cases b; simp
@[simp] lemma bnot_eq_ff_eq_eq_tt (a : bool) : (bnot a = ff) = (a = tt) :=
by cases a; simp
@[simp] lemma coe_ff : ↑ff = false :=
show (ff = tt) = false, by simp
@[simp] lemma coe_tt : ↑tt = true :=
show (tt = tt) = true, by simp