Idris2Doc : Data.Functor.TraverseSt

Data.Functor.TraverseSt

(source)

Definitions

interfaceTraversableSt : (Type->Type) ->Type
  A particular case of sub-traversability with the state monad.

This is not a full traverse because the final state is not returned.
This allows us to implement this interface for (potentially) infinite data types.

This interface has a law connecting to the `Functor` superinterface:
`traverseSt () $ const $ pure . f` must act as `map f`.

Parameters: f
Constraints: Functor f
Methods:
traverseSt : s-> (s->a-> (s, b)) ->fa->fb

Implementations:
TraversableStStream
TraversableStColist
TraversableStLazyList
Traversablef=>TraversableStf
traverseSt : TraversableStf=>s-> (s->a-> (s, b)) ->fa->fb
Totality: total
Visibility: public export
withIndex : TraversableStf=>fa->f (Nat, a)
Totality: total
Visibility: public export
.withIndex : TraversableStf=>fa->f (Nat, a)
Totality: total
Visibility: public export