Equivalences involving Array

def Equiv.arrayEquivList (α : Type u_1) : Array α ≃ List α

The natural equivalence between arrays and lists.

Equations

• Equiv.arrayEquivList α = { toFun := Array.data, invFun := Array.mk, left_inv := ⋯, right_inv := ⋯ }

instance Array.encodable {α : Type u_1} [Encodable α] : Encodable (Array α)

If α is encodable, then so is Array α.

Equations

• Array.encodable = Encodable.ofEquiv (List α) (Equiv.arrayEquivList α)

instance Array.countable {α : Type u_1} [Countable α] : Countable (Array α)

If α is countable, then so is Array α.

Equations

• ⋯ = ⋯