Data.Indexed.Fixed

We can regarding any functor as indexed, with a specified fixed
index.

Definitions

record FixIndex : i -> (Type -> Type) -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

WithIndex : f a -> FixIndex x f a

Projection: 

.unIndex : FixIndex x f a -> f a

Hints:

Filterable f => Filterable (FixIndex x f)

Foldable f => Foldable (FixIndex x f)

Functor f => Functor (FixIndex x f)

Filterable f => IndFilterable i (FixIndex x f)

Foldable f => IndFoldable i (FixIndex x f)

Functor f => IndFunctor i (FixIndex x f)

Traversable f => IndTraversable i (FixIndex x f)

Witherable f => IndWitherable i (FixIndex x f)

Traversable f => Traversable (FixIndex x f)

Witherable f => Witherable (FixIndex x f)

.unIndex : FixIndex x f a -> f a

Visibility: public export

unIndex : FixIndex x f a -> f a

Visibility: public export