Data.String.Iterator(source)

Reexports

Definitions

data StringIterator : String -> Type

Totality: total
Visibility: export

withString : (str : String) -> ((1 _ : StringIterator str) -> a) -> a

Totality: total
Visibility: export

withIteratorString : (str : String) -> (1 _ : StringIterator str) -> (String -> a) -> a

  Runs the action `f` on the slice `res` of the original string `str` represented by the
  iterator `it`

data UnconsResult : String -> Type

Totality: total
Visibility: public export
Constructors:

EOF : UnconsResult str

Character : Char -> (1 _ : StringIterator str) -> UnconsResult str

uncons : (str : String) -> (1 _ : StringIterator str) -> UnconsResult str

foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy

Totality: total
Visibility: export

unpack : String -> LazyList Char

Totality: total
Visibility: export