Data.Inspect.SizedType

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

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

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

param_a : (rec : SizedType a n) -> Type

param_n : (rec : SizedType a n) -> Nat