Idris2Doc : Control.Applicative.Indexing

Control.Applicative.Indexing

(source)
Definitions
record Indexing : Type -> (k -> Type) -> k -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIndexing : (i -> (i, f a)) -> Indexing i f a

  Projection: 
.runIndexing : Indexing i f a -> i -> (i, f a)

  Hints:
  
Applicative f => Applicative (Indexing i f)
  
Contravariant f => Contravariant (Indexing i f)
  
Functor f => Functor (Indexing i f)
.runIndexing : Indexing i f a -> i -> (i, f a)
  Totality: total
  Visibility: public export
runIndexing : Indexing i f a -> i -> (i, f a)
  Totality: total
  Visibility: public export
indexing : Num i => ((a -> Indexing i f b) -> s -> Indexing i f t) -> (i -> a -> f b) -> s -> f t
  Totality: total
  Visibility: public export