Documentation

Mathlib.Logic.Equiv.Array

Equivalences involving Array #

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

The natural equivalence between arrays and lists.

Equations
    Instances For
      instance Array.encodable {α : Type u_1} [Encodable α] :

      If α is encodable, then so is Array α.

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

        If α is countable, then so is Array α.