fact: Definition map (f : A -> B) (p : Parser Toks Tok M A n) : Parser Toks Tok M B n := MkParser (fun _ mlen toks => fmap (Success.map f) (runParser p mlen toks)).
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)