TParsec.Success

MkSuccess : (Value : a) -> (Small : LT Size n) -> (Leftovers : toks Size) -> Success toks a n

record Success toks a n

toks

 

a

 

n

 

MkSuccess : (Value : a) -> (Small : LT Size n) -> (Leftovers : toks Size) -> Success toks a n

Value : (rec : Success toks a n) -> a

Size : (rec : Success toks a n) -> Nat

Small : (rec : Success toks a n) -> LT (Size rec) n

Leftovers : (rec : Success toks a n) -> toks (Size rec)

and : (p : Success toks a n) -> Success toks b (Size p) -> Success toks (a, b) n

complete : Success toks a n -> Maybe a

fromView : All (View toks tok :-> Success toks tok)

getTok : Inspect toks tok => All (toks :-> Maybe :. Success toks tok)

guardM : (a -> Maybe b) -> All (Success toks a :-> Maybe :. Success toks b)

ltLift : LT m n -> Success toks a m -> Success toks a n

lteLift : LTE m n -> Success toks a m -> Success toks a n

map : (f : a -> b) -> All (Success toks a :-> Success toks b)