Agda-2.6.0: A dependently typed functional programming language and proof assistant

Agda.Utils.IndexedList

Synopsis

# Documentation

data Some :: (k -> *) -> * where Source #

Existential wrapper for indexed types.

Constructors

 Some :: f i -> Some f

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

Unpacking a wrapped value.

data All :: (x -> *) -> [x] -> * where Source #

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) Source #

Constructing an indexed list from a plain list.

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

Turning an indexed list back into a plain list.

data Index :: [x] -> x -> * where Source #

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 Source #

Indices are just natural numbers.

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

Mapping over an indexed list.

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

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

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

Looking up an element in an indexed list.

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

All indices into an indexed list.