m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
init : α✝
f : α → α✝ → m (ForInStep α✝)
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ ForInStep.run <$> forIn.visit f t init = forIn (toList t) init f
m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
init : α✝
f : α → α✝ → m (ForInStep α✝)
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ forIn t init f = forIn (toList t) init f
simp [forIn, RBNode.forIn]
no goals
m : Type u_1 → Type u_2
α : Type u_3
α✝ : Type u_1
init : α✝
f : α → α✝ → m (ForInStep α✝)
inst✝¹ : Monad m
inst✝ : LawfulMonad m
t : RBNode α
⊢ ForInStep.run <$> forIn.visit f t init = forIn (toList t) init f
rw [List.forIn_eq_bindList, forIn_visit_eq_bindList]