def Array.Perm {α : Type u_1} (as bs : Array α) : Prop

Perm as bs asserts that as and bs are permutations of each other.

This is a wrapper around List.Perm, and for now has much less API. For more complicated verification, use perm_iff_toList_perm and the List API.

Equations

• as.Perm bs = as.toList.Perm bs.toList

def Array.«term_~_» : Lean.TrailingParserDescr

Perm as bs asserts that as and bs are permutations of each other.

This is a wrapper around List.Perm, and for now has much less API. For more complicated verification, use perm_iff_toList_perm and the List API.

Equations

• Array.«term_~_» = Lean.ParserDescr.trailingNode `Array.«term_~_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

theorem Array.perm_iff_toList_perm {α : Type u_1} {as bs : Array α} : as.Perm bs ↔ as.toList.Perm bs.toList

@[simp]

theorem Array.perm_toArray {α : Type u_1} (as bs : List α) : as.toArray.Perm bs.toArray ↔ as.Perm bs

@[simp]

theorem Array.Perm.refl {α : Type u_1} (xs : Array α) : xs.Perm xs

theorem Array.Perm.rfl {α : Type u_1} {xs : List α} : xs.Perm xs

theorem Array.Perm.of_eq {α : Type u_1} {xs ys : Array α} (h : xs = ys) : xs.Perm ys

theorem Array.Perm.symm {α : Type u_1} {xs ys : Array α} (h : xs.Perm ys) : ys.Perm xs

theorem Array.Perm.trans {α : Type u_1} {xs ys zs : Array α} (h₁ : xs.Perm ys) (h₂ : ys.Perm zs) : xs.Perm zs

instance Array.instTransPerm {α : Type u_1} : Trans Perm Perm Perm

Equations

• Array.instTransPerm = { trans := ⋯ }

theorem Array.perm_comm {α : Type u_1} {xs ys : Array α} : xs.Perm ys ↔ ys.Perm xs

theorem Array.Perm.push {α : Type u_1} (x y : α) {xs ys : Array α} (p : xs.Perm ys) : ((xs.push x).push y).Perm ((ys.push y).push x)

theorem Array.swap_perm {α : Type u_1} {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < xs.size) : (xs.swap i j h₁ h₂).Perm xs