Data.HVect

Reexports

Definitions

data HVect : Vect k Type -> Type

  Heterogeneous vectors where the type index gives, element-wise,
  the types of the contents.

Totality: total
Visibility: public export
Constructors:

Nil : HVect []

(::) : t -> HVect ts -> HVect (t :: ts)

Hints:

DecEq (HVect [])

(DecEq t, DecEq (HVect ts)) => DecEq (HVect (t :: ts))

Eq (HVect [])

(Eq t, Eq (HVect ts)) => Eq (HVect (t :: ts))

Shows len ts => Show (HVect ts)

index : (i : Fin k) -> HVect ts -> index i ts

  Extract an element from an HVect.
  
  ```idris example
  > index 0 (the (HVect _) [1, "string"])
  1
  ```

Totality: total
Visibility: public export

deleteAt : (i : Fin (S l)) -> HVect ts -> HVect (deleteAt i ts)

  Delete an element from an HVect.
  
  ```idris example
  > deleteAt 0 (the (HVect _) [1, "string"])
  ["string"]
  ```

Totality: total
Visibility: public export

replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)

  Replace an element in an HVect.
  
  ```idris example
  > replaceAt 0 "firstString" (the (HVect _) [1, "string"])
  ["firstString", "string"]
  ```

Totality: total
Visibility: public export

updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)

  Update an element in an HVect.
  
  ```idris example
  > updateAt 0 (const True) (the (HVect _) [1, "string"])
  [True, "string"]
  ```

Totality: total
Visibility: public export

(++) : HVect ts -> HVect us -> HVect (ts ++ us)

  Append two `HVect`s.
  
  ```idris example
  > (the (HVect _) [1]) ++ (the (HVect _) ["string"])
  [1, "string"]
  ```

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

consInjective1 : x :: xs = y :: ys -> x = y

Totality: total
Visibility: public export

consInjective2 : x :: xs = y :: ys -> xs = ys

Totality: total
Visibility: public export

interface Shows : (k : Nat) -> Vect k Type -> Type

Parameters: k, ts
Methods:

shows : HVect ts -> Vect k String

Implementations:

Shows 0 []

(Show t, Shows len ts) => Shows (S len) (t :: ts)

shows : Shows k ts => HVect ts -> Vect k String

Totality: total
Visibility: public export

get : (1 _ : HVect ts) -> {auto 1 _ : Elem t ts} -> t

  Extract an arbitrary element of the correct type.
  
  ```idris example
  > get [1, "string"] {p = Here}
  1
  ```

Totality: total
Visibility: public export

put : t -> (1 _ : HVect ts) -> {auto 1 _ : Elem t ts} -> HVect ts

  Replace an element with the correct type. (Homogeneous)
  
  ```idris example
  > put 2 [1, "string"]
  [2, "string"]
  ```

Totality: total
Visibility: public export

htPut : u -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect (replaceByElem ts p u)

  Replace an element with the correct type. (Heterogeneous)
  
  ```idris example
  > htPut True [1, "string"] {p = Here}
  [True, "string"]
  ```

Totality: total
Visibility: public export

update : (t -> t) -> (1 _ : HVect ts) -> {auto 1 _ : Elem t ts} -> HVect ts

  Update an element with the correct type. (Homogeneous)
  
  ```idris example
  > update (const "hello world!") [1, "string"]
  [1, "hello world!"]
  ```

Totality: total
Visibility: public export

htUpdate : (t -> u) -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect (replaceByElem ts p u)

  Update an element with the correct type. (Heterogeneous)
  
  ```idris example
  > htUpdate (\_ : String => 2) [1, "string"]
  [1, 2]
  ```

Totality: total
Visibility: public export