Data.SnocList.HasLength

Definitions

LHasLength : Nat -> List a -> Type

Visibility: public export

data HasLength : Nat -> SnocList a -> Type

Totality: total
Visibility: public export
Constructors:

Z : HasLength 0 [<]

S : HasLength n sa -> HasLength (S n) (sa :< a)

hasLength : HasLength n sx -> length sx = n

Visibility: export

map : (f : (a -> b)) -> HasLength n xs -> HasLength n (map f xs)

Visibility: export

sucL : HasLength n sx -> HasLength (S n) ([<x] ++ sx)

Visibility: export

sucR : HasLength n sx -> HasLength (S n) (sx ++ [<x])

Visibility: export

hlAppend : HasLength m sx -> HasLength n sy -> HasLength (n + m) (sx ++ sy)

Visibility: export

hlFish : HasLength m sx -> LHasLength n ys -> HasLength (n + m) (sx <>< ys)

Visibility: export

mkHasLength : (sx : SnocList a) -> HasLength (length sx) sx

Visibility: export

hlChips : HasLength m sx -> LHasLength n ys -> LHasLength (m + n) (sx <>> ys)

Visibility: export

cast : (0 _ : length sx = length sy) -> HasLength m sx -> HasLength m sy

Visibility: export

hlReverse : HasLength m acc -> HasLength m (reverse acc)

Visibility: export