Idris2Doc : Data.String.Iterator

Data.String.Iterator

data StringIterator : String -> Type
  Totality: total
data UnconsResult : String -> Type
  Totality: total
  Constructors:
  
EOF : UnconsResult str
  
Character : Char -> (1 _ : StringIterator str) -> UnconsResult str
foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
  Totality: total
uncons : (str : String) -> (1 _ : StringIterator str) -> UnconsResult str
unpack : String -> LazyList Char
  Totality: total
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`
withString : (str : String) -> ((1 _ : StringIterator str) -> a) -> a
  Totality: total