Data.Inspect

interface Inspect 

inspect : Inspect As A => All (As :-> Maybe :. View As A)

MkSizedList : (xs : List a) -> SizedList a (length xs)

MkSizedType : (Dict : SizedDict a) -> (Value : a) -> (Sized : sizeFromDict Dict Value = n) -> SizedType a n

SizedList : Type -> Nat -> Type

record SizedType a n

a

 

n

 

MkSizedType : (Dict : SizedDict a) -> (Value : a) -> (Sized : sizeFromDict Dict Value = n) -> SizedType a n

Dict : (rec : SizedType a n) -> SizedDict a

Value : (rec : SizedType a n) -> a

Sized : (rec : SizedType a n) -> sizeFromDict (Dict rec) (Value rec) = n

View : (as : Nat -> Type) -> (a : Type) -> (n : Nat) -> Type