def Bottleneck (α : Type) : Type

Equations

• Bottleneck α = α

@[implicit_reducible]

instance instReprBottleneck {α : Type} [i : Repr α] : Repr (Bottleneck α)

Equations

• instReprBottleneck = { reprPrec := reprPrec }

@[implicit_reducible]

instance instLEBottleneck {α : Type} [LE α] : LE (Bottleneck α)

Equations

• instLEBottleneck = instLEBottleneck._aux_1

@[implicit_reducible]

instance instPartialOrderBottleneck {α : Type} [PartialOrder α] : PartialOrder (Bottleneck α)

Equations

• instPartialOrderBottleneck = instPartialOrderBottleneck._aux_1

@[implicit_reducible]

instance instLinearOrderBottleneck {α : Type} [LinearOrder α] : LinearOrder (Bottleneck α)

Equations

• instLinearOrderBottleneck = instLinearOrderBottleneck._aux_1

@[implicit_reducible]

instance instAddBottleneckOfLinearOrder {α : Type} [LinearOrder α] : Add (Bottleneck α)

Equations

• instAddBottleneckOfLinearOrder = { add := max }

@[implicit_reducible]

instance instMulBottleneckOfLinearOrder {α : Type} [LinearOrder α] : Mul (Bottleneck α)

Equations

• instMulBottleneckOfLinearOrder = { mul := min }

@[simp]

theorem Bottleneck.add_eq_max {α : Type} [LinearOrder α] {a b : Bottleneck α} : a + b = max a b

@[simp]

theorem Bottleneck.mul_eq_min {α : Type} [LinearOrder α] {a b : Bottleneck α} : a * b = min a b

@[implicit_reducible]

instance instBotBottleneck {α : Type} [Bot α] : Bot (Bottleneck α)

Equations

• instBotBottleneck = instBotBottleneck._aux_1

@[implicit_reducible]

instance instOrderBotBottleneck {α : Type} [LE α] [OrderBot α] : OrderBot (Bottleneck α)

Equations

• instOrderBotBottleneck = instOrderBotBottleneck._aux_1

@[implicit_reducible]

instance instTopBottleneck {α : Type} [Top α] : Top (Bottleneck α)

Equations

• instTopBottleneck = instTopBottleneck._aux_1

@[implicit_reducible]

instance instOrderTopBottleneck {α : Type} [LE α] [OrderTop α] : OrderTop (Bottleneck α)

Equations

• instOrderTopBottleneck = instOrderTopBottleneck._aux_1

@[implicit_reducible]

instance instZeroBottleneckOfOrderBot {α : Type} [LE α] [OrderBot α] : Zero (Bottleneck α)

Equations

• instZeroBottleneckOfOrderBot = { zero := ⊥ }

@[simp]

theorem Bottlenext.zero_eq_bot {α : Type} [LE α] [OrderBot α] : 0 = ⊥

@[implicit_reducible]

instance instOneBottleneckOfOrderTop {α : Type} [LE α] [OrderTop α] : One (Bottleneck α)

Equations

• instOneBottleneckOfOrderTop = { one := ⊤ }

@[simp]

theorem Bottlenext.one_eq_top {α : Type} [LE α] [OrderTop α] : 1 = ⊤

@[implicit_reducible]

instance instSemiringBottleneckOfOrderBotOfOrderTop {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : Semiring (Bottleneck α)

Equations

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

instance instIsPositiveOrderedAddMonoidBottleneck {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : IsPositiveOrderedAddMonoid (Bottleneck α)

instance instCanonicallyOrderedAddBottleneckOfOrderBotOfOrderTop {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : CanonicallyOrderedAdd (Bottleneck α)

instance instMulLeftMonoBottleneckOfOrderBotOfOrderTop {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : MulLeftMono (Bottleneck α)

instance instMulRightMonoBottleneckOfOrderBotOfOrderTop {α : Type} [LinearOrder α] [OrderBot α] [OrderTop α] : MulRightMono (Bottleneck α)

@[implicit_reducible]

instance instOmegaCompletePartialOrderBottleneckOfCompleteLinearOrder {α : Type} [CompleteLinearOrder α] : OmegaCompletePartialOrder (Bottleneck α)

Equations

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

instance instOmegaContinuousNonUnitalSemiringBottleneck {α : Type} [CompleteLinearOrder α] : OmegaContinuousNonUnitalSemiring (Bottleneck α)

@[implicit_reducible]

instance instKStarBottleneckOfTop {α : Type} [Top α] : KStar (Bottleneck α)

Equations

• instKStarBottleneckOfTop = { kstar := fun (x : Bottleneck α) => ⊤ }

instance instLawfulKStarBottleneck {α : Type} [CompleteLinearOrder α] : LawfulKStar (Bottleneck α)

instance instCountableBottleneck {α : Type} [Countable α] : Countable (Bottleneck α)

def Secutiy₄ : Type

Equations

• Secutiy₄ = Fin 4

def Secutiy₄.toFin (s : Secutiy₄) : Fin 4

Equations

• s.toFin = s

@[implicit_reducible]

instance instLinearOrderSecutiy₄ : LinearOrder Secutiy₄

Equations

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

@[implicit_reducible]

instance instOrderBotSecutiy₄ : OrderBot Secutiy₄

Equations

• instOrderBotSecutiy₄ = { bot := instOrderBotSecutiy₄._aux_1, bot_le := instOrderBotSecutiy₄._proof_3 }

@[implicit_reducible]

instance instOrderTopSecutiy₄ : OrderTop Secutiy₄

Equations

• instOrderTopSecutiy₄ = { top := instOrderTopSecutiy₄._aux_1, le_top := instOrderTopSecutiy₄._proof_3 }

def P : Pol[Fin 3,ℕ,Bottleneck Secutiy₄]

Equations

• P = wnk_pol {~0 ← ~3}

@[implicit_reducible]

instance instOfNatBottleneck {α : Type} {x : ℕ} [OfNat α x] : OfNat (Bottleneck α) x

Equations

• instOfNatBottleneck = instOfNatBottleneck._aux_1

@[implicit_reducible]

instance instOfNatSecutiy₄OfNatNat : OfNat Secutiy₄ 0

Equations

• instOfNatSecutiy₄OfNatNat = { ofNat := ⟨0, instOfNatSecutiy₄OfNatNat._proof_1⟩ }

@[implicit_reducible]

instance instOfNatSecutiy₄OfNatNat_1 : OfNat Secutiy₄ 1

Equations

• instOfNatSecutiy₄OfNatNat_1 = { ofNat := ⟨1, instOfNatSecutiy₄OfNatNat_1._proof_1⟩ }

@[implicit_reducible]

instance instOfNatSecutiy₄OfNatNat_2 : OfNat Secutiy₄ 2

Equations

• instOfNatSecutiy₄OfNatNat_2 = { ofNat := ⟨2, instOfNatSecutiy₄OfNatNat_2._proof_1⟩ }

@[implicit_reducible]

instance instOfNatSecutiy₄OfNatNat_3 : OfNat Secutiy₄ 3

Equations

• instOfNatSecutiy₄OfNatNat_3 = { ofNat := ⟨3, instOfNatSecutiy₄OfNatNat_3._proof_1⟩ }

@[implicit_reducible]

instance instReprSecutiy₄ : Repr Secutiy₄

Equations

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

def EENat : Type

Equations

• EENat = WithBot ℕ∞

@[implicit_reducible]

instance instOfNatEENat (n : ℕ) : OfNat EENat n

Equations

• instOfNatEENat n = { ofNat := some (some n) }

@[implicit_reducible]

instance instLinearOrderEENat : LinearOrder EENat

Equations

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

@[implicit_reducible]

instance instOrderBotEENat : OrderBot EENat

Equations

• instOrderBotEENat = { bot := instOrderBotEENat._aux_1, bot_le := instOrderBotEENat._proof_3 }

@[implicit_reducible]

instance instOrderTopEENat : OrderTop EENat

Equations

• instOrderTopEENat = { top := instOrderTopEENat._aux_1, le_top := instOrderTopEENat._proof_3 }

@[implicit_reducible]

instance instReprENat_weightedNetKAT : Repr ℕ∞

Equations

• instReprENat_weightedNetKAT = { reprPrec := fun (p : ℕ∞) (n : ℕ) => if p = ⊤ then Std.Format.text "⊤" else reprPrec p.toNat n }

@[implicit_reducible]

instance instReprEENat : Repr EENat

Equations

• instReprEENat = { reprPrec := fun (p : EENat) (n : ℕ) => if p = ⊤ then Std.Format.text "⊤" else if p = ⊥ then Std.Format.text "⊥" else reprPrec (Option.get! p).toNat n }