forall {α : Type} {β : Type}, (β -> α -> β) -> β -> (forall (as : Array.{0} α), (optParam.{1} Nat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) -> (optParam.{1} Nat (Array.size.{0} α as)) -> β)
fun {α : Type} {β : Type} (f : β -> α -> β) (init : β) (as : Array.{0} α) (start : Nat) (stop : Nat) => Id.run.{0} β (Array.foldlM.{0, 0, 0} α β Id.{0} Id.instMonad.{0} (fun (x1._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26 : β) (x2._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26 : α) => Pure.pure.{0, 0} Id.{0} (Applicative.toPure.{0, 0} Id.{0} (Monad.toApplicative.{0, 0} Id.{0} Id.instMonad.{0})) β (f x1._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26 x2._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26)) init as start stop)
fun {α : Type} {β : Type.{v}} (f : β -> α -> β) (init : β) (as : Array.{0} α) (start : Nat) (stop : Nat) => Id.run.{v} β (Array.foldlM.{0, v, v} α β Id.{v} Id.instMonad.{v} (fun (x1._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26 : β) (x2._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26 : α) => Pure.pure.{v, v} Id.{v} (Applicative.toPure.{v, v} Id.{v} (Monad.toApplicative.{v, v} Id.{v} Id.instMonad.{v})) β (f x1._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26 x2._@.Init.Data.Array.Basic.1478953397._hygCtx._hyg.26)) init as start stop)