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

Safe HaskellSafe




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

Existential wrapper for indexed types.


Some :: f i -> Some f 

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

Unpacking a wrapped value.

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


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

An index into a type-level list.


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.