Idris2Doc : Syntax.IHateParens.List

Syntax.IHateParens.List

(source)

Definitions

.length : List a -> Nat
Totality: total
Visibility: public export
.asVect : (xs : List a) -> Vect (xs .length) a
Totality: total
Visibility: public export
.withIdx : (xs : List a) -> List (Fin (xs .length), a)
Totality: total
Visibility: public export