Documentation

Std.Classes.Ord.Vector

Instances for Vector #

instance Vector.instReflCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.ReflCmp cmp] {n : Nat} :
instance Vector.instLawfulEqCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.LawfulEqCmp cmp] {n : Nat} :
instance Vector.instLawfulBEqCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [BEq α] [Std.LawfulBEqCmp cmp] {n : Nat} :
instance Vector.instOrientedCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.OrientedCmp cmp] {n : Nat} :
instance Vector.instTransCmpCompareLex {α : Type u_1} {cmp : ααOrdering} [Std.TransCmp cmp] {n : Nat} :
instance Vector.instReflOrd {α : Type u_1} [Ord α] [Std.ReflOrd α] {n : Nat} :
instance Vector.instLawfulEqOrd {α : Type u_1} [Ord α] [Std.LawfulEqOrd α] {n : Nat} :
instance Vector.instLawfulBEqOrd {α : Type u_1} [Ord α] [BEq α] [Std.LawfulBEqOrd α] {n : Nat} :
instance Vector.instOrientedOrd {α : Type u_1} [Ord α] [Std.OrientedOrd α] {n : Nat} :
instance Vector.instTransOrd {α : Type u_1} [Ord α] [Std.TransOrd α] {n : Nat} :