Documentation

Init.Data.Ord.Vector

Instances for `Vector` #

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

Equations

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

Instances For

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)