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

chore: helper simp theorems

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-29 23:05:48 -08:00
parent 3e45060dd5
commit bc21716bad
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/SimpLemmas.lean
View file

@ -124,6 +124,8 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
@[simp] theorem Bool.not_false : (!false) = true := by decide
@[simp] theorem Bool.not_beq_true (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
@[simp] theorem Bool.not_beq_false (b : Bool) : (!(b == false)) = (b == true) := by cases b <;> rfl
@[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
@[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
@[simp] theorem Bool.beq_to_eq (a b : Bool) :
(a == b) = (a = b) := by cases a <;> cases b <;> decide