fact: Fixpoint make_path (db : state_fmap) (targetb : state -> bool) (play : state -> move -> option state) (x : state) (fuel : nat) := match fuel with | O => None | S p => if targetb x then Some nil else match find db x with | None => None | Some m => match play x m with | Some y => match make_path db targetb play y p with | None => None | Some l => Some (m :: l) end | None => None end end end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL