@[inline]

def Array.compareLex {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) : Ordering

Equations

• Array.compareLex cmp a₁ a₂ = Array.compareLex.go cmp a₁ a₂ 0

@[specialize #[]]

def Array.compareLex.go {α : Type u_1} (cmp : α → α → Ordering) (a₁ a₂ : Array α) (i : Nat) : Ordering

Equations

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

@[instance_reducible]

instance Array.instOrd {α : Type u_1} [Ord α] : Ord (Array α)

Equations

• Array.instOrd = { compare := Array.compareLex compare }

theorem Array.compare_eq_compareLex {α : Type u_1} [Ord α] : compare = Array.compareLex compare

theorem List.compareLex_eq_compareLex_toArray {α : Type u_1} {cmp : α → α → Ordering} {l₁ l₂ : List α} : List.compareLex cmp l₁ l₂ = Array.compareLex cmp l₁.toArray l₂.toArray

theorem List.compare_eq_compare_toArray {α : Type u_1} [Ord α] {l₁ l₂ : List α} : compare l₁ l₂ = compare l₁.toArray l₂.toArray

theorem Array.compareLex_eq_compareLex_toList {α : Type u_1} {cmp : α → α → Ordering} {a₁ a₂ : Array α} : Array.compareLex cmp a₁ a₂ = List.compareLex cmp a₁.toList a₂.toList

theorem Array.compare_eq_compare_toList {α : Type u_1} [Ord α] {a₁ a₂ : Array α} : compare a₁ a₂ = compare a₁.toList a₂.toList