Idris2Doc : Data.String.Iterator

Data.String.Iterator

StringIterator : String -> Type
Totality: total
UnconsResult : String -> Type
Totality: total
Constructors:
EOF : UnconsResultstr
Character : Char -> (1 _ : StringIteratorstr) -> UnconsResultstr
foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
Totality: total
uncons : (str : String) -> (1 _ : StringIteratorstr) -> UnconsResultstr
unpack : String -> LazyList Char
Totality: total
withIteratorString : (str : String) -> (1 _ : StringIteratorstr) -> (String -> a) -> a
Runs the action `f` on the slice `res` of the original string `str` represented by the
iterator `it`
withString : (str : String) -> ((1 _ : StringIteratorstr) -> a) -> a
Totality: total