Idris2Doc : Data.HVect

Data.HVect

Reexports

importpublic Data.Vect

Definitions

dataHVect : VectkType->Type
  Heterogeneous vectors where the type index gives, element-wise,
the types of the contents.

Totality: total
Visibility: public export
Constructors:
Nil : HVect []
(::) : t->HVectts->HVect (t::ts)

Hints:
DecEq (HVect [])
(DecEqt, DecEq (HVectts)) =>DecEq (HVect (t::ts))
Eq (HVect [])
(Eqt, Eq (HVectts)) =>Eq (HVect (t::ts))
Showslents=>Show (HVectts)
index : (i : Fink) ->HVectts->indexits
  Extract an element from an HVect.

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

Totality: total
Visibility: public export
deleteAt : (i : Fin (Sl)) ->HVectts->HVect (deleteAtits)
  Delete an element from an HVect.

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

Totality: total
Visibility: public export
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
Visibility: public export
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
Visibility: public export
(++) : HVectts->HVectus->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
interfaceShows : (k : Nat) ->VectkType->Type
Parameters: k, ts
Methods:
shows : HVectts->VectkString

Implementations:
Shows0 []
(Showt, Showslents) =>Shows (Slen) (t::ts)
shows : Showskts=>HVectts->VectkString
Totality: total
Visibility: public export
get : (1_ : HVectts) -> {auto1_ : Elemtts} ->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_ : HVectts) -> {auto1_ : Elemtts} ->HVectts
  Replace an element with the correct type. (Homogeneous)

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

Totality: total
Visibility: public export
htPut : u-> (1_ : HVectts) -> {auto1p : Elemtts} ->HVect (replaceByElemtspu)
  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_ : HVectts) -> {auto1_ : Elemtts} ->HVectts
  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_ : HVectts) -> {auto1p : Elemtts} ->HVect (replaceByElemtspu)
  Update an element with the correct type. (Heterogeneous)

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

Totality: total
Visibility: public export