Idris2Doc : Data.Linear.Traverse1

Data.Linear.Traverse1

(source)

Reexports

importpublic Data.Linear.Token

Definitions

interfaceFoldable1 : (Type->Type) ->Type
  Folds over a computation including potentially linear
mutable state.

Parameters: f
Methods:
foldl1 : (a->e->F1sa) ->a->fe->F1sa
foldr1 : (e->a->F1sa) ->a->fe->F1sa
foldMap1 : Monoidm=> (a->F1sm) ->fa->F1sm
traverse1_ : (a->F1's) ->fa->F1's

Implementations:
Foldable1Maybe
Foldable1 (Eithere)
Foldable1List
Foldable1SnocList
Foldable1 (Vectn)
Foldable1List1
foldl1 : Foldable1f=> (a->e->F1sa) ->a->fe->F1sa
Totality: total
Visibility: public export
foldr1 : Foldable1f=> (e->a->F1sa) ->a->fe->F1sa
Totality: total
Visibility: public export
foldMap1 : Foldable1f=>Monoidm=> (a->F1sm) ->fa->F1sm
Totality: total
Visibility: public export
traverse1_ : Foldable1f=> (a->F1's) ->fa->F1's
Totality: total
Visibility: public export
for1_ : Foldable1f=>fa-> (a->F1's) ->F1's
  Flipped version of `traverse1_`

Totality: total
Visibility: export
foldl1List : (a->e->F1sa) ->a->Liste->F1sa
Totality: total
Visibility: export
foldr1SnocList : (e->a->F1sa) ->a->SnocListe->F1sa
Totality: total
Visibility: export
foldr1List : (e->a->F1sa) ->a->Liste->F1sa
Totality: total
Visibility: export
foldl1SnocList : (a->e->F1sa) ->a->SnocListe->F1sa
Totality: total
Visibility: export
foldMap1List : Monoidm=> (a->F1sm) ->Lista->F1sm
Totality: total
Visibility: export
foldMap1SnocList : Monoidm=> (a->F1sm) ->SnocLista->F1sm
Totality: total
Visibility: export
traverse1_List : (a->F1's) ->Lista->F1's
Totality: total
Visibility: export
traverse1_SnocList : (a->F1's) ->SnocLista->F1's
Totality: total
Visibility: export
foldl1Vect : (a->e->F1sa) ->a->Vectne->F1sa
Totality: total
Visibility: export
foldr1Vect : (e->a->F1sa) ->a->Vectne->F1sa
Totality: total
Visibility: export
foldMap1Vect : Monoidm=> (a->F1sm) ->Vectna->F1sm
Totality: total
Visibility: export
traverse1_Vect : (a->F1's) ->Vectna->F1's
Totality: total
Visibility: export
interfaceTraversable1 : (Type->Type) ->Type
Parameters: f
Constraints: Foldable1 f
Methods:
traverse1 : (a->F1sb) ->fa->F1s (fb)

Implementations:
Traversable1Maybe
Traversable1 (Eithere)
Traversable1List
Traversable1SnocList
Traversable1 (Vectn)
Traversable1List1
traverse1 : Traversable1f=> (a->F1sb) ->fa->F1s (fb)
Totality: total
Visibility: public export
traverse1List : SnocListb-> (a->F1sb) ->Lista->F1s (Listb)
Totality: total
Visibility: export
traverse1SnocList : Listb-> (a->F1sb) ->SnocLista->F1s (SnocListb)
Totality: total
Visibility: export
traverse1Vect : (sx : SnocListb) -> (a->F1sb) ->Vectna->F1s (Vect (lengthsx+n) b)
Totality: total
Visibility: export
for1 : Traversable1f=>fa-> (a->F1sb) ->F1s (fb)
  Flipped version of `traverse1`

Totality: total
Visibility: export
zipWithIndex : Traversable1f=>fa->f (Nat, a)
  Pairs each value in a data structure with its index of appearance.

Totality: total
Visibility: export