Documentation

WeightedNetKAT.Examples.Abilene

Abilene #

This file contains a simplified version of the Abilene network

source
def List.sum' {α : Type u_1} [Add α] [Zero α] (a : List α) :
α

A version of List.sum that doesn't leave a trailing 0

Useful for non-AddZeroClass instances of add.

Equations
Instances For
    source
    def Array.sum' {α : Type u_1} [Add α] [Zero α] (a : Array α) :
    α

    A version of Array.sum that doesn't leave a trailing 0

    Useful for non-AddZeroClass instances of add.

    Equations
    Instances For
      source
      inductive WeightedNetKAT.Abilene.Switch :
      Type
      Instances For
        source
        @[implicit_reducible]
        instance WeightedNetKAT.Abilene.instDecidableEqSwitch :
        DecidableEq Switch
        Equations
        source
        @[implicit_reducible]
        instance WeightedNetKAT.Abilene.instFintypeSwitch :
        Fintype Switch
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def WeightedNetKAT.Abilene.instInhabitedSwitch.default :
        Switch
        Equations
        Instances For
          source
          @[implicit_reducible]
          instance WeightedNetKAT.Abilene.instInhabitedSwitch :
          Inhabited Switch
          Equations
          source
          def WeightedNetKAT.Abilene.instReprSwitch.repr :
          Switch → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            instance WeightedNetKAT.Abilene.instReprSwitch :
            Repr Switch
            Equations
            source
            @[implicit_reducible]
            instance WeightedNetKAT.Abilene.instListedSwitch :
            Listed Switch
            Equations
            • One or more equations did not get rendered due to their size.
            source
            inductive WeightedNetKAT.Abilene.City :
            Type
            Instances For
              source
              @[implicit_reducible]
              instance WeightedNetKAT.Abilene.instDecidableEqCity :
              DecidableEq City
              Equations
              source
              @[implicit_reducible]
              instance WeightedNetKAT.Abilene.instFintypeCity :
              Fintype City
              Equations
              • One or more equations did not get rendered due to their size.
              source
              @[implicit_reducible]
              instance WeightedNetKAT.Abilene.instInhabitedCity :
              Inhabited City
              Equations
              source
              def WeightedNetKAT.Abilene.instInhabitedCity.default :
              City
              Equations
              Instances For
                source
                def WeightedNetKAT.Abilene.instReprCity.repr :
                City → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[implicit_reducible]
                  instance WeightedNetKAT.Abilene.instReprCity :
                  Repr City
                  Equations
                  source
                  @[implicit_reducible]
                  instance WeightedNetKAT.Abilene.instListedCity :
                  Listed City
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[implicit_reducible]
                  instance WeightedNetKAT.Abilene.instToFormatPkSwitchCity :
                  Std.ToFormat Pk[Switch,City]
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[implicit_reducible, instance 1000000]
                  instance WeightedNetKAT.Abilene.instReprRunSwitchCityOfToFormat {Q : Type} [Std.ToFormat Q] :
                  Repr rReachability.Run
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[implicit_reducible]
                  instance WeightedNetKAT.Abilene.instToFormatSSwitchCity {𝒮 : Type u_1} {p : RPol 𝒮} :
                  Std.ToFormat (S p)
                  Equations
                  source
                  def WeightedNetKAT.Abilene.mod {𝒮 : Type u_2} [Semiring 𝒮] {α : Type u_1} (c : α) :
                  RPol 𝒮
                  Equations
                  Instances For
                    source
                    def WeightedNetKAT.Abilene.test {𝒮 : Type u_2} [Semiring 𝒮] {α : Type u_1} (c : α) :
                    RPol 𝒮
                    Equations
                    Instances For
                      source
                      def WeightedNetKAT.Abilene.latency :
                      City → City → Option Weighted.Arctic
                      Equations
                      Instances For
                        source
                        def WeightedNetKAT.Abilene.latency.ms (val : Weighted.Arctic) :
                        Option Weighted.Arctic
                        Equations
                        Instances For
                          source
                          def WeightedNetKAT.Abilene.bandwidth :
                          City → City → Option Weighted.Bottleneck
                          Equations
                          Instances For
                            source
                            def WeightedNetKAT.Abilene.bandwidth.mbps (val : Weighted.Bottleneck) :
                            Option Weighted.Bottleneck
                            Equations
                            Instances For
                              source
                              theorem WeightedNetKAT.Abilene.bandwidth_is_symm {a b : City} :
                              bandwidth a b = bandwidth b a
                              source
                              @[simp]
                              theorem WeightedNetKAT.Abilene.OrderRingIso.ωSum_nat_eq_of_lawfulkstar {α : Type u_1} {β : Type u_2} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] [Semiring β] [OmegaCompletePartialOrder β] [OrderBot β] [IsPositiveOrderedAddMonoid β] [KStar β] [LawfulKStar β] [MulLeftMono β] [MulRightMono β] [OmegaContinuousNonUnitalSemiring β] (e : α ≃+*o β) (f : ℕ → α) :
                              e (ω∑ (i : ℕ), f i) = ω∑ (i : ℕ), e (f i)
                              source
                              @[simp]
                              theorem WeightedNetKAT.Abilene.OrderRingIso.kstar_eq_of_lawfulkstar {α : Type u_1} {β : Type u_2} [Semiring α] [OmegaCompletePartialOrder α] [OrderBot α] [IsPositiveOrderedAddMonoid α] [KStar α] [LawfulKStar α] [MulLeftMono α] [MulRightMono α] [OmegaContinuousNonUnitalSemiring α] [Semiring β] [OmegaCompletePartialOrder β] [OrderBot β] [IsPositiveOrderedAddMonoid β] [KStar β] [LawfulKStar β] [MulLeftMono β] [MulRightMono β] [OmegaContinuousNonUnitalSemiring β] (e : α ≃+*o β) (a : α) :
                              e (KStar.kstar a) = KStar.kstar (e a)
                              source
                              def WeightedNetKAT.Abilene.build_of_rel {α β : Type} [Listed α] [DecidableEq α] [Semiring β] (r : α → α → Option β) :
                              RPol β
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def WeightedNetKAT.Abilene.run :
                                IO Unit
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For