Instances for Vector

@[inline]

def Vector.compareLex {α : Type u_1} {n : Nat} (cmp : α → α → Ordering) (a b : Vector α n) : Ordering

Equations

• Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray

@[instance_reducible]

instance Vector.instOrd {α : Type u_1} {n : Nat} [Ord α] : Ord (Vector α n)

Equations

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

theorem Vector.compareLex_eq_compareLex_toArray {α : Type u_1} {n : Nat} {cmp : α → α → Ordering} {a b : Vector α n} : Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray

theorem Vector.compareLex_eq_compareLex_toList {α : Type u_1} {n : Nat} {cmp : α → α → Ordering} {a b : Vector α n} : Vector.compareLex cmp a b = List.compareLex cmp a.toList b.toList

theorem Vector.compare_eq_compare_toArray {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} : compare a b = compare a.toArray b.toArray

theorem Vector.compare_eq_compare_toList {α : Type u_1} {n : Nat} [Ord α] {a b : Vector α n} : compare a b = compare a.toList b.toList

instance Vector.instReflCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {n : Nat} : Std.ReflCmp (Vector.compareLex cmp)

instance Vector.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] {n : Nat} : Std.LawfulEqCmp (Vector.compareLex cmp)

instance Vector.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [BEq α] [Std.LawfulBEqCmp cmp] {n : Nat} : Std.LawfulBEqCmp (Vector.compareLex cmp)

instance Vector.instOrientedCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {n : Nat} : Std.OrientedCmp (Vector.compareLex cmp)

instance Vector.instTransCmpCompareLex {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {n : Nat} : Std.TransCmp (Vector.compareLex cmp)

instance Vector.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] {n : Nat} : Std.ReflOrd (Vector α n)

instance Vector.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] {n : Nat} : Std.LawfulEqOrd (Vector α n)

instance Vector.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] {n : Nat} : Std.LawfulBEqOrd (Vector α n)

instance Vector.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] {n : Nat} : Std.OrientedOrd (Vector α n)

instance Vector.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] {n : Nat} : Std.TransOrd (Vector α n)

theorem Vector.compareLex_append_append {α : Type u_1} {cmp : α → α → Ordering} {n m : Nat} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m} : Vector.compareLex cmp (xs₁ ++ ys₁) (xs₂ ++ ys₂) = (Vector.compareLex cmp xs₁ xs₂).then (Vector.compareLex cmp ys₁ ys₂)

theorem Vector.compare_append_append {α : Type u_1} [Ord α] {n m : Nat} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m} : compare (xs₁ ++ ys₁) (xs₂ ++ ys₂) = (compare xs₁ xs₂).then (compare ys₁ ys₂)

theorem Vector.compareLex_map_map {α : Type u_2} {cmp : α → α → Ordering} {n : Nat} {β : Type u_1} {cmp' : β → β → Ordering} (f : α → β) (hf : ∀ (a b : α), cmp' (f a) (f b) = cmp a b) {xs ys : Vector α n} : Vector.compareLex cmp' (map f xs) (map f ys) = Vector.compareLex cmp xs ys

theorem Vector.compare_map_map {α : Type u_1} [Ord α] {n : Nat} {β : Type u_2} [Ord β] (f : α → β) (hf : ∀ (a b : α), compare (f a) (f b) = compare a b) {xs ys : Vector α n} : compare (map f xs) (map f ys) = compare xs ys

theorem Vector.compareLex_flatMap_flatMap {α : Type u_2} {cmp : α → α → Ordering} {n m : Nat} {β : Type u_1} {cmp' : β → β → Ordering} [Std.LawfulEqCmp cmp] [Std.LawfulEqCmp cmp'] (f : α → Vector β m) (hf : ∀ (a b : α), Vector.compareLex cmp' (f a) (f b) = cmp a b) (hm : 0 < m) {xs ys : Vector α n} : Vector.compareLex cmp' (xs.flatMap f) (ys.flatMap f) = Vector.compareLex cmp xs ys

theorem Vector.compare_flatMap_flatMap {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] {n m : Nat} {β : Type u_2} [Ord β] [Std.LawfulEqOrd β] (f : α → Vector β m) (hf : ∀ (a b : α), compare (f a) (f b) = compare a b) (hm : 0 < m) {xs ys : Vector α n} : compare (xs.flatMap f) (ys.flatMap f) = compare xs ys