fact: Definition guardM (f : A -> option B) : Success Toks Tok A n -> option (Success Toks Tok B n) := fun s => option_map (fun b => MkSuccess b (small s) (leftovers s)) (f (value s)).
imports: parseque(Indexed Sized) Coq(PeanoNat)