Documentation

DY.ALaCarte.Ordering

def DY.ALaCarte.Container.compare {CtorId : Type} {ctors : Ctors CtorId} [Ord CtorId] [Std.LawfulEqOrd CtorId] [(id : CtorId) → Ord (ctors id).Data] (x1 x2 : Container ctors) :

Equations

x1.compare x2 = DY.ALaCarte.BareContainer.compare✝ x1.val x2.val

Instances For

theorem DY.ALaCarte.Container.compare.compare_self {CtorId : Type} {ctors : Ctors CtorId} [Ord CtorId] [Std.LawfulEqOrd CtorId] [(id : CtorId) → Ord (ctors id).Data] [∀ (id : CtorId), Std.ReflOrd (ctors id).Data] (x : Container ctors) :

x.compare x = Ordering.eq

theorem DY.ALaCarte.Container.compare.eq_of_compare {CtorId : Type} {ctors : Ctors CtorId} [Ord CtorId] [Std.LawfulEqOrd CtorId] [(id : CtorId) → Ord (ctors id).Data] [∀ (id : CtorId), Std.LawfulEqOrd (ctors id).Data] (x1 x2 : Container ctors) :

x1.compare x2 = Ordering.eq → x1 = x2

theorem DY.ALaCarte.Container.compare.eq_swap {CtorId : Type} {ctors : Ctors CtorId} [Ord CtorId] [Std.LawfulEqOrd CtorId] [Std.OrientedOrd CtorId] [(id : CtorId) → Ord (ctors id).Data] [∀ (id : CtorId), Std.OrientedOrd (ctors id).Data] (x1 x2 : Container ctors) :

x1.compare x2 = (x2.compare x1).swap

theorem DY.ALaCarte.Container.compare.isLE_trans {CtorId : Type} {ctors : Ctors CtorId} [Ord CtorId] [Std.LawfulEqOrd CtorId] [Std.TransOrd CtorId] [(id : CtorId) → Ord (ctors id).Data] [∀ (id : CtorId), Std.LawfulEqOrd (ctors id).Data] [∀ (id : CtorId), Std.TransOrd (ctors id).Data] (x1 x2 x3 : Container ctors) :

(x1.compare x2).isLE = true → (x2.compare x3).isLE = true → (x1.compare x3).isLE = true

class DY.ALaCarte.RepresentableOrd (f : Type → Type) [FunctorSizeOf f] [Representable f] :

ctoridOrd : Ord (Representable.CtorId f)
ctoridOrd_lawfulEq : Std.LawfulEqOrd (Representable.CtorId f)
ctoridOrd_trans : Std.TransOrd (Representable.CtorId f)
ctorDataOrd (id : Representable.CtorId f) : Ord (Representable.ctors id).Data
ctorDataOrd_lawfulEq (id : Representable.CtorId f) : Std.LawfulEqOrd (Representable.ctors id).Data
ctorDataOrd_trans (id : Representable.CtorId f) : Std.TransOrd (Representable.ctors id).Data

Instances

@[instance_reducible]

def DY.ALaCarte.instOrdCtorIdOfRepresentableOrd (f : Type → Type) [FunctorSizeOf f] [Representable f] [inst : RepresentableOrd f] :

Ord (Representable.CtorId f)

Equations

DY.ALaCarte.instOrdCtorIdOfRepresentableOrd f = DY.ALaCarte.RepresentableOrd.ctoridOrd

Instances For

theorem DY.ALaCarte.instLawfulEqOrdCtorId (f : Type → Type) [FunctorSizeOf f] [Representable f] [inst : RepresentableOrd f] :

Std.LawfulEqOrd (Representable.CtorId f)

@[instance_reducible]

def DY.ALaCarte.instOrdDataCtorsOfRepresentableOrd (f : Type → Type) [FunctorSizeOf f] [Representable f] [inst : RepresentableOrd f] (id : Representable.CtorId f) :

Ord (Representable.ctors id).Data

Equations

DY.ALaCarte.instOrdDataCtorsOfRepresentableOrd f id = DY.ALaCarte.RepresentableOrd.ctorDataOrd id

Instances For

@[instance_reducible]

instance DY.ALaCarte.instOrdContainerForOfRepresentableOrd (f : Type → Type) [FunctorSizeOf f] [Representable f] [RepresentableOrd f] :

Ord (ContainerFor f)

Equations

DY.ALaCarte.instOrdContainerForOfRepresentableOrd f = { compare := DY.ALaCarte.Container.compare }

instance DY.ALaCarte.instReflOrdContainerFor (f : Type → Type) [FunctorSizeOf f] [Representable f] [RepresentableOrd f] :

Std.ReflOrd (ContainerFor f)

instance DY.ALaCarte.instLawfulEqOrdContainerFor (f : Type → Type) [FunctorSizeOf f] [Representable f] [RepresentableOrd f] :

Std.LawfulEqOrd (ContainerFor f)

instance DY.ALaCarte.instOrientedOrdContainerFor (f : Type → Type) [FunctorSizeOf f] [Representable f] [RepresentableOrd f] :

Std.OrientedOrd (ContainerFor f)

instance DY.ALaCarte.instTransOrdContainerFor (f : Type → Type) [FunctorSizeOf f] [Representable f] [RepresentableOrd f] :

Std.TransOrd (ContainerFor f)

def DY.ALaCarte.FunctorUnion.CtorId.compare {a : Type} [Ord a] [Std.LawfulEqOrd a] {fs : a → Type → Type} [(id : a) → FunctorSizeOf (fs id)] [(id : a) → Representable (fs id)] [(id : a) → RepresentableOrd (fs id)] (x1 x2 : CtorId fs) :

Equations

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

Instances For

theorem DY.ALaCarte.FunctorUnion.CtorId.compare.compare_self {a : Type} [Ord a] [Std.LawfulEqOrd a] {fs : a → Type → Type} [(id : a) → FunctorSizeOf (fs id)] [(id : a) → Representable (fs id)] [(id : a) → RepresentableOrd (fs id)] (x : CtorId fs) :

x.compare x = Ordering.eq

theorem DY.ALaCarte.FunctorUnion.CtorId.compare.eq_of_compare {a : Type} [Ord a] [Std.LawfulEqOrd a] {fs : a → Type → Type} [(id : a) → FunctorSizeOf (fs id)] [(id : a) → Representable (fs id)] [(id : a) → RepresentableOrd (fs id)] (x1 x2 : CtorId fs) :

x1.compare x2 = Ordering.eq → x1 = x2

theorem DY.ALaCarte.FunctorUnion.CtorId.compare.eq_swap {a : Type} [Ord a] [Std.LawfulEqOrd a] [Std.OrientedOrd a] {fs : a → Type → Type} [(id : a) → FunctorSizeOf (fs id)] [(id : a) → Representable (fs id)] [(id : a) → RepresentableOrd (fs id)] (x1 x2 : CtorId fs) :

x1.compare x2 = (x2.compare x1).swap

theorem DY.ALaCarte.FunctorUnion.CtorId.compare.isLE_trans {a : Type} [Ord a] [Std.LawfulEqOrd a] [Std.TransOrd a] {fs : a → Type → Type} [(id : a) → FunctorSizeOf (fs id)] [(id : a) → Representable (fs id)] [(id : a) → RepresentableOrd (fs id)] (x1 x2 x3 : CtorId fs) :

(x1.compare x2).isLE = true → (x2.compare x3).isLE = true → (x1.compare x3).isLE = true

@[instance_reducible]

instance DY.ALaCarte.instRepresentableOrdFunctorUnionOfLawfulEqOrdOfTransOrd {a : Type} [Ord a] [Std.LawfulEqOrd a] [Std.TransOrd a] (fs : a → Type → Type) [(id : a) → FunctorSizeOf (fs id)] [(id : a) → Representable (fs id)] [(id : a) → RepresentableOrd (fs id)] :

RepresentableOrd (FunctorUnion fs)

Equations

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