Idris2Doc : Data.HVect

Data.HVect

(++) : HVectts -> HVectus -> HVect (ts++us)
  Append two `HVect`s.

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

Totality: total
Fixity Declaration: infixr operator, level 7
dataHVect : VectkType -> Type
  Heterogeneous vectors where the type index gives, element-wise,
the types of the contents.

Totality: total
Constructors:
Nil : HVect []
(::) : t -> HVectts -> HVect (t::ts)
interfaceShows : (k : Nat) -> VectkType -> Type
Parameters: k, ts
Methods:
shows : HVectts -> VectkString

Implementations:
Shows0 []
(Showt, Showslents) => Shows (Slen) (t::ts)
consInjective1 : x::xs = y::ys -> x = y
Totality: total
consInjective2 : x::xs = y::ys -> xs = ys
Totality: total
deleteAt : (i : Fin (Sl)) -> HVectts -> HVect (deleteAtits)
  Delete an element from an HVect.

```idris example
> deleteAt 0 (the (HVect _) [1, "string"])
["string"]
```

Totality: total
get : (1 _ : HVectts) -> {auto 1 _ : Elemtts} -> t
  Extract an arbitrary element of the correct type.

```idris example
> get [1, "string"] {p = Here}
1
```

Totality: total
htPut : u -> (1 _ : HVectts) -> {auto 1 p : Elemtts} -> HVect (replaceByElemtspu)
  Replace an element with the correct type. (Heterogeneous)

```idris example
> htPut True [1, "string"] {p = Here}
[True, "string"]
```

Totality: total
htUpdate : (t -> u) -> (1 _ : HVectts) -> {auto 1 p : Elemtts} -> HVect (replaceByElemtspu)
  Update an element with the correct type. (Heterogeneous)

```idris example
> htUpdate (\_ : String => 2) [1, "string"]
[1, 2]
```

Totality: total
index : (i : Fink) -> HVectts -> indexits
  Extract an element from an HVect.

```idris example
> index 0 (the (HVect _) [1, "string"])
1
```

Totality: total
put : t -> (1 _ : HVectts) -> {auto 1 _ : Elemtts} -> HVectts
  Replace an element with the correct type. (Homogeneous)

```idris example
> put 2 [1, "string"]
[2, "string"]
```

Totality: total
replaceAt : (i : Fink) -> t -> HVectts -> HVect (replaceAtitts)
  Replace an element in an HVect.

```idris example
> replaceAt 0 "firstString" (the (HVect _) [1, "string"])
["firstString", "string"]
```

Totality: total
shows : Showskts => HVectts -> VectkString
Totality: total
update : (t -> t) -> (1 _ : HVectts) -> {auto 1 _ : Elemtts} -> HVectts
  Update an element with the correct type. (Homogeneous)

```idris example
> update (const "hello world!") [1, "string"]
[1, "hello world!"]
```

Totality: total
updateAt : (i : Fink) -> (indexits -> t) -> HVectts -> HVect (replaceAtitts)
  Update an element in an HVect.

```idris example
> updateAt 0 (const True) (the (HVect _) [1, "string"])
[True, "string"]
```

Totality: total