HasSize class

A type has a size in units of β when it embeds into Vector β size. A duplex sponge over units β absorbs and squeezes elements of such a type size units at a time.

Ported verbatim from ArkLib (ArkLib/Data/Classes/HasSize.lean).

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 α β)