fact: Definition dfs' : V -> list V -> m (list V) := mfix_multi (V :: list V :: nil) (list V) (fun rec from seen => if list_in_dec from seen then ret (m:=m) seen else foldM (fun v acc => if list_in_dec v acc then ret (m:=m) acc else rec v acc) (ret (m:=m) seen) (successors g from)).
imports: Coq.Lists.List Coq.PArith.BinPos ExtLib.Structures.Monads ExtLib.Structures.Reducible ExtLib.Data.Graph.Graph ExtLib.Data.Monads.FuelMonad ExtLib.Data.Monads.IdentityMonad ExtLib.Data.List ExtLib.Core.RelDec