Data.Sized.Builtin
type
Ordinal
n
type
Sized
f n