Equivalences involving Array

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

The natural equivalence between arrays and lists.

Equations

• One or more equations did not get rendered due to their size.

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

• (_ : Countable (Array α)) = (_ : Countable (Array α))