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) : Ordering

Equations

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

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] : Type

• 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

@[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

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

@[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) : Ordering

Equations

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

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.