Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.IndexedList

Synopsis
  • data Some (a :: k -> Type) where
    • Some :: forall {k} (a :: k -> Type) (i :: k). a i -> Some a
  • withSome :: Some b -> (forall (i :: k). b i -> a) -> a
  • data All (a :: x -> Type) (b :: [x]) where
    • Nil :: forall {x} (a :: x -> Type). All a ('[] :: [x])
    • Cons :: forall {x} (a :: x -> Type) (x1 :: x) (xs :: [x]). a x1 -> All a xs -> All a (x1 ': xs)
  • makeAll :: forall {x} a (b :: x -> Type). (a -> Some b) -> [a] -> Some (All b)
  • forgetAll :: forall {x} b a (xs :: [x]). (forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
  • data Index (a :: [x]) (b :: x) where
    • Zero :: forall {x} (b :: x) (xs :: [x]). Index (b ': xs) b
    • Suc :: forall {x} (xs :: [x]) (b :: x) (y :: x). Index xs b -> Index (y ': xs) b
  • forgetIndex :: forall {x1} (xs :: [x1]) (x2 :: x1). Index xs x2 -> Int
  • mapWithIndex :: forall {x} (xs :: [x]) p q. (forall (x1 :: x). Index xs x1 -> p x1 -> q x1) -> All p xs -> All q xs
  • lIndex :: forall {x1} (xs :: [x1]) (x2 :: x1) (p :: x1 -> Type). Index xs x2 -> Lens' (All p xs) (p x2)
  • lookupIndex :: forall {x1} p (xs :: [x1]) (x2 :: x1). All p xs -> Index xs x2 -> p x2
  • allIndices :: forall {x} (p :: x -> Type) (xs :: [x]). All p xs -> All (Index xs) xs

Documentation

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

Existential wrapper for indexed types.

Constructors

Some :: forall {k} (a :: k -> Type) (i :: k). a i -> Some a 

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

Unpacking a wrapped value.

data All (a :: x -> Type) (b :: [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 :: forall {x} (a :: x -> Type). All a ('[] :: [x]) 
Cons :: forall {x} (a :: x -> Type) (x1 :: x) (xs :: [x]). a x1 -> All a xs -> All a (x1 ': xs) 

makeAll :: forall {x} a (b :: x -> Type). (a -> Some b) -> [a] -> Some (All b) Source #

Constructing an indexed list from a plain list.

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

Turning an indexed list back into a plain list.

data Index (a :: [x]) (b :: x) where Source #

An index into a type-level list.

Constructors

Zero :: forall {x} (b :: x) (xs :: [x]). Index (b ': xs) b 
Suc :: forall {x} (xs :: [x]) (b :: x) (y :: x). Index xs b -> Index (y ': xs) b 

forgetIndex :: forall {x1} (xs :: [x1]) (x2 :: x1). Index xs x2 -> Int Source #

Indices are just natural numbers.

mapWithIndex :: forall {x} (xs :: [x]) p q. (forall (x1 :: x). Index xs x1 -> p x1 -> q x1) -> All p xs -> All q xs Source #

Mapping over an indexed list.

lIndex :: forall {x1} (xs :: [x1]) (x2 :: x1) (p :: x1 -> Type). Index xs x2 -> Lens' (All p xs) (p x2) Source #

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

lookupIndex :: forall {x1} p (xs :: [x1]) (x2 :: x1). All p xs -> Index xs x2 -> p x2 Source #

Looking up an element in an indexed list.

allIndices :: forall {x} (p :: x -> Type) (xs :: [x]). All p xs -> All (Index xs) xs Source #

All indices into an indexed list.