α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : IsLawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = ↑(foldrM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : IsLawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = List.foldrM f x (toList xs)
change _ = foldrM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs) x
no goals
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : IsLawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = ↑(foldrM.ofFreeMonoid f) (↑FreeMonoid.ofList (toList xs)) x
simp only [foldrm, toList_spec, foldMap_hom_free (foldrM.ofFreeMonoid f),
  foldrm.ofFreeMonoid_comp_of, foldrM.get, FreeMonoid.ofList_toList]