fact: Fixpoint mapAccumL {A X Y : Type} (f : A -> X -> (A * Y)) (s : A) (v : list X) : A * list Y := match v with | nil => (s, nil) | x :: xs => let (s', y) := f s x in let (s'', ys) := mapAccumL f s' xs in (s'', y :: ys) end.
imports: Hask.Ltac Hask.Control.Monad Hask.Data.Eq Hask.Data.Maybe Coq.Program.Wf Coq.Sorting.Sorted Coq.Classes.RelationClasses Coq.Lists.List