TParsec.Success.Success

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

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

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

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

param_a : (rec : Success toks a n) -> Type

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

param_toks : (rec : Success toks a n) -> Nat -> Type

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