Libraries.Data.List.SizeOf

Definitions

record SizeOf : List a -> Type

Totality: total
Visibility: public export
Constructor: 

MkSizeOf : (size : Nat) -> (0 _ : HasLength size xs) -> SizeOf xs

Projections:

0 .hasLength : ({rec:0} : SizeOf xs) -> HasLength (size {rec:0}) xs

.size : SizeOf xs -> Nat

.size : SizeOf xs -> Nat

Totality: total
Visibility: public export

size : SizeOf xs -> Nat

Totality: total
Visibility: public export

0 .hasLength : ({rec:0} : SizeOf xs) -> HasLength (size {rec:0}) xs

Totality: total
Visibility: public export

0 hasLength : ({rec:0} : SizeOf xs) -> HasLength (size {rec:0}) xs

Totality: total
Visibility: public export

0 theList : SizeOf xs -> List a

Totality: total
Visibility: export

zero : SizeOf []

Totality: total
Visibility: public export

suc : SizeOf as -> SizeOf (a :: as)

Totality: total
Visibility: public export

sucR : SizeOf as -> SizeOf (as ++ [a])

Totality: total
Visibility: export

(+) : SizeOf xs -> SizeOf ys -> SizeOf (xs ++ ys)

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 8

mkSizeOf : (xs : List a) -> SizeOf xs

Totality: total
Visibility: export

reverse : SizeOf xs -> SizeOf (reverse xs)

Totality: total
Visibility: export

map : SizeOf xs -> SizeOf (map f xs)

Totality: total
Visibility: export

take : SizeOf (take n xs)

Totality: total
Visibility: export

data SizedView : SizeOf as -> Type

Totality: total
Visibility: public export
Constructors:

Z : SizedView (MkSizeOf 0 Z)

S : (n : SizeOf as) -> SizedView (suc n)

sizedView : (p : SizeOf as) -> SizedView p

Totality: total
Visibility: export