inductive WeightedNetKAT.Fields : Type

• dst : Fields
• pt : Fields
• sw : Fields

@[implicit_reducible]

instance WeightedNetKAT.instDecidableEqFields : DecidableEq Fields

Equations

• WeightedNetKAT.instDecidableEqFields x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance WeightedNetKAT.instFintypeFields : Fintype Fields

Equations

• WeightedNetKAT.instFintypeFields = { elems := { val := ↑WeightedNetKAT.Fields.enumList, nodup := WeightedNetKAT.Fields.enumList_nodup }, complete := WeightedNetKAT.instFintypeFields._proof_1 }

@[implicit_reducible]

instance WeightedNetKAT.instListedFields : Listed Fields

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.instEncodableFields : Encodable Fields

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.instReprFields : Repr Fields

Equations

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

@[reducible, inline]

abbrev WeightedNetKAT.H₁ : ℕ

Equations

• WeightedNetKAT.H₁ = 1

@[reducible, inline]

abbrev WeightedNetKAT.H₂ : ℕ

Equations

• WeightedNetKAT.H₂ = 2

@[reducible, inline]

abbrev WeightedNetKAT.H₃ : ℕ

Equations

• WeightedNetKAT.H₃ = 3

@[reducible, inline]

abbrev WeightedNetKAT.H₄ : ℕ

Equations

• WeightedNetKAT.H₄ = 4

@[reducible, inline]

abbrev WeightedNetKAT.S₂ : ℕ

Equations

• WeightedNetKAT.S₂ = 2

@[reducible, inline]

abbrev WeightedNetKAT.S₃ : ℕ

Equations

• WeightedNetKAT.S₃ = 3

@[reducible, inline]

abbrev WeightedNetKAT.S₄ : ℕ

Equations

• WeightedNetKAT.S₄ = 4

@[reducible, inline]

abbrev WeightedNetKAT.S₅ : ℕ

Equations

• WeightedNetKAT.S₅ = 5

def WeightedNetKAT.Network {F N 𝒮 : Type} (ingress : Pred[F,N]) (p l : Pol[F,N,𝒮]) (egress : Pred[F,N]) : Pol[F,N,𝒮]

Equations

• WeightedNetKAT.Network ingress p l egress = wnk_pol {~(WeightedNetKAT.Pol.Filter ingress); dup; (~p; ~l; dup)*; ~p; ~(WeightedNetKAT.Pol.Filter egress)}

def WeightedNetKAT.«command#wnk_eval[_,_,_]{_}» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.S.repr {F N 𝒮 : Type} [Listed F] {p : RPol 𝒮} (s : S p) : String

Equations

• s_2.repr = "♡"
• s_2.repr = "♡"
• s_2.repr = "♡"
• s_2.repr = "♡"
• WeightedNetKAT.S.repr (Sum.inl PUnit.unit) = "♡"
• WeightedNetKAT.S.repr (Sum.inr PUnit.unit) = "♣"
• WeightedNetKAT.S.repr (Sum.inl x) = toString "l" ++ toString x.repr
• WeightedNetKAT.S.repr (Sum.inr x) = toString "r" ++ toString x.repr
• WeightedNetKAT.S.repr (Sum.inl x) = toString "l" ++ toString x.repr
• WeightedNetKAT.S.repr (Sum.inr x) = toString "r" ++ toString x.repr
• s_2.repr = s_2.repr
• WeightedNetKAT.S.repr (Sum.inl s_3) = s_3.repr
• WeightedNetKAT.S.repr (Sum.inr Unit) = "♡*"

@[implicit_reducible]

instance WeightedNetKAT.instReprS {F N 𝒮 : Type} [Listed F] {p : RPol 𝒮} : Repr (S p)

Equations

• WeightedNetKAT.instReprS = { reprPrec := fun (s : WeightedNetKAT.S p) (x : ℕ) => Std.Format.text s.repr }

@[implicit_reducible]

instance WeightedNetKAT.instReprProdUnit_weightedNetKAT {X : Type} [Repr X] : Repr (Unit × X)

Equations

• WeightedNetKAT.instReprProdUnit_weightedNetKAT = { reprPrec := fun (x : Unit × X) (n : ℕ) => reprPrec x.2 n }

@[implicit_reducible]

instance WeightedNetKAT.instReprProdUnit_weightedNetKAT_1 {X : Type} [Repr X] : Repr (X × Unit)

Equations

• WeightedNetKAT.instReprProdUnit_weightedNetKAT_1 = { reprPrec := fun (x : X × Unit) (n : ℕ) => reprPrec x.1 n }

def WeightedNetKAT.RPol.eval {F N 𝒮 : Type} [Fintype F] [DecidableEq F] [Fintype N] [DecidableEq N] [Listed F] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq 𝒮] [KStar 𝒮] [Repr 𝒮] [Repr F] [Repr N] (p : RPol 𝒮) : IO Std.Format

Equations

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

def WeightedNetKAT.RPol.eval_string {F N 𝒮 : Type} [Fintype F] [DecidableEq F] [Fintype N] [DecidableEq N] [Listed F] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq 𝒮] [KStar 𝒮] (p : RPol 𝒮) (s : GS F N) : 𝒮

Equations

• p.eval_string s = p.ewnka.sem s

@[implicit_reducible]

instance WeightedNetKAT.myRepr {α A B : Type} [DecidableEq α] [Zero α] [DecidableEq A] [DecidableEq B] [Listed A] [Listed B] [Repr α] [Repr A] [Repr B] : Repr (Matrix A B α)

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.instReprWNKASOfFintypeOfInhabitedOfListedPkOfIsPositiveOrderedAddMonoidOfDecidableEqOfKStar {F N 𝒮 : Type} [Fintype F] [DecidableEq F] [Fintype N] [DecidableEq N] [Listed F] [Listed N] [Inhabited N] [Listed Pk[F,N]] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [DecidableEq 𝒮] [KStar 𝒮] [Repr 𝒮] [Repr F] [Repr N] (p : RPol 𝒮) : Repr WNKA[F,N,𝒮,S p]

Equations

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

def WeightedNetKAT.«command#wnka_eval[_,_,_]{_}» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«command#wnka_dot[_,_,_]{_}» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«command#wnka_eval_str[_,_,_]{_}(_)» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«command#wnka_eval'[_,_,_]{_}» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.pk_entry.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.pk_entry : Category

Equations

• Lean.Parser.Category.pk_entry = { }

def WeightedNetKAT.«pk_entry_↦_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«termPk[_]» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_match_case~_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_match_case.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwnk_match_case : Category

Equations

• Lean.Parser.Category.cwnk_match_case = { }

def WeightedNetKAT.cwnk_match_case : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_match_case|_↦_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_match_case|_↦__1» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_match_case|_=>_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_match_case|_=>__1» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_polMatch_ : Lean.ParserDescr

Equations

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