Agda.Utils.IndexedList

Documentation

data Some :: (k -> Type) -> Type where

Existential wrapper for indexed types.

Constructors

Some :: f i -> Some f

withSome :: Some b -> (forall i. b i -> a) -> a

Unpacking a wrapped value.

data All :: (x -> Type) -> [x] -> Type where

Lists indexed by a type-level list. A value of type All p [x₁..xₙ] is a sequence of values of types p x₁, .., p xₙ.

Constructors

Nil :: All p '[]

Cons :: p x -> All p xs -> All p (x ': xs)

makeAll :: (a -> Some b) -> [a] -> Some (All b)

Constructing an indexed list from a plain list.

forgetAll :: (forall x. b x -> a) -> All b xs -> [a]

Turning an indexed list back into a plain list.

data Index :: [x] -> x -> Type where

An index into a type-level list.

Constructors

Zero :: Index (x ': xs) x

Suc :: Index xs x -> Index (y ': xs) x

forgetIndex :: Index xs x -> Int

Indices are just natural numbers.

mapWithIndex :: (forall x. Index xs x -> p x -> q x) -> All p xs -> All q xs

Mapping over an indexed list.

lIndex :: Index xs x -> Lens' (p x) (All p xs)

If you have an index you can get a lens for the given element.

lookupIndex :: All p xs -> Index xs x -> p x

Looking up an element in an indexed list.

allIndices :: All p xs -> All (Index xs) xs

All indices into an indexed list.