Libraries.Data.SnocList.SizeOf

Definitions

0 LSizeOf : List a -> Type

Visibility: public export

record SizeOf : SnocList a -> Type

Totality: total
Visibility: public export
Constructor: 

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

Projections:

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

.size : SizeOf sx -> Nat

.size : SizeOf sx -> Nat

Totality: total
Visibility: public export

size : SizeOf sx -> Nat

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

0 theList : SizeOf sx -> SnocList a

Totality: total
Visibility: export

Lin : SizeOf [<]

Totality: total
Visibility: public export

(:<) : SizeOf as -> (0 a : {a:4018}) -> SizeOf (as :< a)

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 7

zero : SizeOf [<]

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

sucL : SizeOf as -> SizeOf ([<a] ++ as)

Totality: total
Visibility: export

(<><) : SizeOf sx -> LSizeOf ys -> SizeOf (sx <>< ys)

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 7

(<>>) : SizeOf sx -> LSizeOf ys -> LSizeOf (sx <>> ys)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 6

cast : LSizeOf xs -> SizeOf (cast xs)

Totality: total
Visibility: export

(+) : SizeOf sx -> SizeOf sy -> SizeOf (sx ++ sy)

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

mkSizeOf : (sx : SnocList a) -> SizeOf sx

Totality: total
Visibility: export

reverse : SizeOf sx -> SizeOf (reverse sx)

Totality: total
Visibility: export

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

Totality: total
Visibility: export

data SizedView : SizeOf as -> Type

Totality: total
Visibility: public export
Constructors:

Z : SizedView [<]

S : (n : SizeOf as) -> SizedView (n :< a)

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

Totality: total
Visibility: export