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} (l : Array α) : l.Perm l

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

theorem Array.Perm.of_eq {α : Type u_1} {l₁ l₂ : Array α} (h : l₁ = l₂) : l₁.Perm l₂

theorem Array.Perm.symm {α : Type u_1} {l₁ l₂ : Array α} (h : l₁.Perm l₂) : l₂.Perm l₁

theorem Array.Perm.trans {α : Type u_1} {l₁ l₂ l₃ : Array α} (h₁ : l₁.Perm l₂) (h₂ : l₂.Perm l₃) : l₁.Perm l₃

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

Equations

• Array.instTransPerm = { trans := ⋯ }

theorem Array.perm_comm {α : Type u_1} {l₁ l₂ : Array α} : l₁.Perm l₂ ↔ l₂.Perm l₁

theorem Array.Perm.push {α : Type u_1} (x y : α) {l₁ l₂ : Array α} (p : l₁.Perm l₂) : ((l₁.push x).push y).Perm ((l₂.push y).push x)

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