ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.IndexedList

datadata Some (a :: k -> Type) where

Existential wrapper for indexed types.

valuewithSome :: Some b -> (forall (i :: k). b i -> a) -> a

Unpacking a wrapped value.

datadata All (a :: x -> Type) (b :: [x]) 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ₙ.

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

Constructing an indexed list from a plain list.

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

Turning an indexed list back into a plain list.

datadata Index (a :: [x]) (b :: x) where

An index into a type-level list.

valueforgetIndex :: Index xs x2 -> Int

Indices are just natural numbers.

valuemapWithIndex

Mapping over an indexed list.

valuelIndex :: Index xs x2 -> Lens' (All p xs) (p x2)

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

valuelookupIndex :: All p xs -> Index xs x2 -> p x2

Looking up an element in an indexed list.

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

All indices into an indexed list.