HasSize class

class HasSize (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

Type class for types that has an injective mapping to a vector of a given length size of another type (often UInt8).

• size : ℕ
• toFun : α ↪ Vector β (size α β)