fact: Definition andbind (p : Parser Toks Tok M A n) (q : A -> Box (Parser Toks Tok M B) n) : Parser Toks Tok M (A * B) n := MkParser (fun _ mlen ts => bind (runParser p mlen ts) (fun sa => let salen := Nat.le_trans _ _ _ (small sa) mlen in let adjust := Success.and sa in fmap adjust (runParser (call (q (value sa)) salen) (Nat.le_refl _) (leftovers sa)))).
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)