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

chore: clenaup test

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-08 18:19:15 -08:00
parent 23319da6c0
commit 0c29987a82
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/do_eqv.lean
View file

@ -1,9 +1,6 @@
theorem byCases_Bool_bind [Monad m] (x : m Bool) (f g : Bool → m β) (isTrue : f true = g true) (isFalse : f false = g false) : (x >>= f) = (x >>= g) := by
have f = g by
funext b
cases b with
| true => exact isTrue
| false => exact isFalse
funext b; cases b <;> assumption
rw [this]
theorem eq_findM [Monad m] [LawfulMonad m] (p : α → m Bool) (xs : List α) :
@ -16,7 +13,7 @@ theorem eq_findM [Monad m] [LawfulMonad m] (p : α → m Bool) (xs : List α) :
xs.findM? p := by
induction xs with simp [List.findM?]
| cons x xs ih =>
rw[← ih]; simp
rw [← ih]; simp
apply byCases_Bool_bind <;> simp
theorem eq_findSomeM_findM [Monad m] [LawfulMonad m] (p : α → m Bool) (xss : List (List α)) :