structure WeightedNetKAT.Pk (F : Type u_4) (N : Type u_5) [Listed F] : Type u_5

• data : Vector N (Listed.size F)

@[implicit_reducible]

instance WeightedNetKAT.instDecidableEqPk {F✝ : Type u_4} {N✝ : Type u_5} {inst✝ : Listed F✝} [DecidableEq F✝] [DecidableEq N✝] : DecidableEq Pk[F✝,N✝]

Equations

• WeightedNetKAT.instDecidableEqPk = WeightedNetKAT.instDecidableEqPk.decEq

def WeightedNetKAT.instDecidableEqPk.decEq {F✝ : Type u_4} {N✝ : Type u_5} {inst✝ : Listed F✝} [DecidableEq F✝] [DecidableEq N✝] (x✝ x✝¹ : Pk[F✝,N✝]) : Decidable (x✝ = x✝¹)

Equations

• WeightedNetKAT.instDecidableEqPk.decEq { data := a } { data := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def WeightedNetKAT.instInhabitedPk.default {a✝ : Type u_4} {a✝¹ : Type u_5} [Inhabited a✝¹] {a✝² : Listed a✝} : Pk[a✝,a✝¹]

Equations

• WeightedNetKAT.instInhabitedPk.default = { data := default }

@[implicit_reducible]

instance WeightedNetKAT.instInhabitedPk {a✝ : Type u_4} {a✝¹ : Type u_5} [Inhabited a✝¹] {a✝² : Listed a✝} : Inhabited Pk[a✝,a✝¹]

Equations

• WeightedNetKAT.instInhabitedPk = { default := WeightedNetKAT.instInhabitedPk.default }

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

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.instFunLikePk {F : Type u_2} [Listed F] {N : Type u_3} : FunLike Pk[F,N] F N

Equations

• WeightedNetKAT.instFunLikePk = { coe := fun (f : Pk[F,N]) (i : F) => f.data[Listed.encodeFin i], coe_injective' := ⋯ }

def WeightedNetKAT.Pk.fill {F : Type u_2} [Listed F] {N : Type u_3} (x : N) : Pk[F,N]

Equations

• WeightedNetKAT.Pk.fill x = { data := Vector.ofFn fun (x_1 : Fin (Listed.size F)) => x }

def WeightedNetKAT.Pk.ofFn {F : Type u_2} [Listed F] {N : Type u_3} (f : F → N) : Pk[F,N]

Equations

• WeightedNetKAT.Pk.ofFn f = { data := Vector.ofFn fun (i : Fin (Listed.size F)) => f (Listed.decodeFin i) }

@[implicit_reducible]

instance WeightedNetKAT.Pk.listed {F : Type u_2} [Listed F] {N : Type u_3} [Listed N] : Listed Pk[F,N]

Equations

• WeightedNetKAT.Pk.listed = Listed.lift { toFun := fun (x : Vector N (Listed.size F)) => { data := x }, invFun := fun (x : Pk[F,N]) => x.data, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance WeightedNetKAT.Pk.fintype {F : Type u_2} [Listed F] {N : Type u_3} [Listed N] : Fintype Pk[F,N]

Equations

• WeightedNetKAT.Pk.fintype = Listed.fintype

@[implicit_reducible]

instance WeightedNetKAT.Pk.ofNat {F : Type u_2} [Listed F] {N : Type u_3} {n : ℕ} [OfNat N n] : OfNat Pk[F,N] n

Equations

• WeightedNetKAT.Pk.ofNat = { ofNat := WeightedNetKAT.Pk.fill (OfNat.ofNat n) }

@[implicit_reducible]

instance WeightedNetKAT.instReprPk {N : Type u_3} {F : Type u_4} [Listed F] [Repr F] [Repr N] : Repr Pk[F,N]

Equations

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

def WeightedNetKAT.«termH[_,_]» : Lean.ParserDescr

Equations

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

@[implicit_reducible]

instance WeightedNetKAT.instDecidableEqProdPkList {F : Type u_2} [Listed F] [DecidableEq F] {N : Type u_3} [DecidableEq N] : DecidableEq (Pk[F,N] × List Pk[F,N])

Equations

• WeightedNetKAT.instDecidableEqProdPkList a b = instDecidableEqProd a b

instance WeightedNetKAT.instCountableProdPkListOfListed {F : Type u_2} [Listed F] {N : Type u_3} [Listed N] : Countable (Pk[F,N] × List Pk[F,N])

inductive WeightedNetKAT.Pred (F : Type u_4) (N : Type u_5) : Type (max u_4 u_5)

• Bool {F : Type u_4} {N : Type u_5} (b : _root_.Bool) : Pred[F,N]
• Test {F : Type u_4} {N : Type u_5} (f : F) (n : N) : Pred[F,N]
• Dis {F : Type u_4} {N : Type u_5} (t u : Pred[F,N]) : Pred[F,N]
• Con {F : Type u_4} {N : Type u_5} (t u : Pred[F,N]) : Pred[F,N]
• Not {F : Type u_4} {N : Type u_5} (t : Pred[F,N]) : Pred[F,N]

def WeightedNetKAT.«termPred[_,_]» : Lean.ParserDescr

Equations

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

inductive WeightedNetKAT.Pol (F : Type u_4) (N : Type u_5) (W : Type u_6) : Type (max (max u_4 u_5) u_6)

• Filter {F : Type u_4} {N : Type u_5} {W : Type u_6} (t : Pred[F,N]) : Pol[F,N,W]
• Mod {F : Type u_4} {N : Type u_5} {W : Type u_6} (f : F) (n : N) : Pol[F,N,W]
• Dup {F : Type u_4} {N : Type u_5} {W : Type u_6} : Pol[F,N,W]
• Seq {F : Type u_4} {N : Type u_5} {W : Type u_6} (p q : Pol[F,N,W]) : Pol[F,N,W]
• Weight {F : Type u_4} {N : Type u_5} {W : Type u_6} (w : W) (p : Pol[F,N,W]) : Pol[F,N,W]
• Add {F : Type u_4} {N : Type u_5} {W : Type u_6} (p q : Pol[F,N,W]) : Pol[F,N,W]
• Iter {F : Type u_4} {N : Type u_5} {W : Type u_6} (p : Pol[F,N,W]) : Pol[F,N,W]

def WeightedNetKAT.«termPol[_,_,_]» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.declare_syntax_cat' : Lean.ParserDescr

Equations

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

def WeightedNetKAT.declare_syntax_cat'? : Lean.ParserDescr

Equations

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

def WeightedNetKAT.commandDeclare_syntax_cat'?_ : Lean.ParserDescr

Equations

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

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

Equations

• WeightedNetKAT.«cwnk_field~_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_field~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

def WeightedNetKAT.cwnk_field.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwnk_field : Category

Equations

• Lean.Parser.Category.cwnk_field = { }

def WeightedNetKAT.cwnk_field : Lean.ParserDescr

Equations

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

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

Equations

• WeightedNetKAT.«cwnk_nat~_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_nat~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

def WeightedNetKAT.cwnk_nat.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwnk_nat : Category

Equations

• Lean.Parser.Category.cwnk_nat = { }

def WeightedNetKAT.cwnk_nat : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_weight.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwnk_weight : Category

Equations

• Lean.Parser.Category.cwnk_weight = { }

def WeightedNetKAT.cwnk_weight : Lean.ParserDescr

Equations

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

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

Equations

• WeightedNetKAT.«cwnk_weight~_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_weight~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

def WeightedNetKAT.cwnk_pred.quot : Lean.ParserDescr

Equations

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

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

Equations

• WeightedNetKAT.«cwnk_pred~_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_pred~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

def Lean.Parser.Category.cwnk_pred : Category

Equations

• Lean.Parser.Category.cwnk_pred = { }

def WeightedNetKAT.cwnk_pred : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_pol : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwnk_pol : Category

Equations

• Lean.Parser.Category.cwnk_pol = { }

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

Equations

• WeightedNetKAT.«cwnk_pol~_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_pol~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

def WeightedNetKAT.cwnk_pol.quot : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«termWnk_pol[_,_,_]_{_}» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_field_ : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_field_ = Lean.ParserDescr.node `WeightedNetKAT.cwnk_field_ 1022 (Lean.ParserDescr.cat `term 1024)

def WeightedNetKAT.cwnk_nat_ : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_nat_ = Lean.ParserDescr.node `WeightedNetKAT.cwnk_nat_ 1022 (Lean.ParserDescr.cat `term 1024)

def WeightedNetKAT.cwnk_weight_ : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_weight_ = Lean.ParserDescr.node `WeightedNetKAT.cwnk_weight_ 1022 (Lean.ParserDescr.const `num)

def WeightedNetKAT.cwnk_nat__1 : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_nat__1 = Lean.ParserDescr.node `WeightedNetKAT.cwnk_nat__1 1022 (Lean.ParserDescr.const `num)

def WeightedNetKAT.cwnk_pred_ : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_pred_ = Lean.ParserDescr.node `WeightedNetKAT.cwnk_pred_ 1022 (Lean.ParserDescr.const `ident)

def WeightedNetKAT.«cwnk_pred_=_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_pred_∨_» : Lean.TrailingParserDescr

Equations

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

def WeightedNetKAT.«cwnk_pred_∧_» : Lean.TrailingParserDescr

Equations

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

def WeightedNetKAT.«cwnk_pred¬_» : Lean.ParserDescr

Equations

• WeightedNetKAT.«cwnk_pred¬_» = Lean.ParserDescr.node `WeightedNetKAT.«cwnk_pred¬_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `cwnk_pred 0))

def WeightedNetKAT.«cwnk_pred(_)» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_pol_ : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_pol_ = Lean.ParserDescr.node `WeightedNetKAT.cwnk_pol_ 1022 (Lean.ParserDescr.cat `cwnk_pred 0)

def WeightedNetKAT.«cwnk_pol_←_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_polDup : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_polDup = Lean.ParserDescr.node `WeightedNetKAT.cwnk_polDup 1024 (Lean.ParserDescr.symbol "dup")

def WeightedNetKAT.«cwnk_pol_;_» : Lean.TrailingParserDescr

Equations

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

def WeightedNetKAT.«cwnk_pol_⨀_» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_pol_⨁_» : Lean.TrailingParserDescr

Equations

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

def WeightedNetKAT.«cwnk_pol_*» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«cwnk_pol_*» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«cwnk_pol_*» 1022 0 (Lean.ParserDescr.symbol "*")

def WeightedNetKAT.«cwnk_pol(_)» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.«cwnk_pol@filter__» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_polSkip : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_polSkip = Lean.ParserDescr.node `WeightedNetKAT.cwnk_polSkip 1024 (Lean.ParserDescr.symbol "skip")

def WeightedNetKAT.cwnk_polDrop : Lean.ParserDescr

Equations

• WeightedNetKAT.cwnk_polDrop = Lean.ParserDescr.node `WeightedNetKAT.cwnk_polDrop 1024 (Lean.ParserDescr.symbol "drop")

def WeightedNetKAT.cwnk_polIf___Then___Else__ : Lean.ParserDescr

Equations

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

def WeightedNetKAT.cwnk_polWhile___Do__ : Lean.ParserDescr

Equations

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

def WeightedNetKAT.Pred.unexpandBool : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pred.unexpandNot : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pred.unexpandDis : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pred.unexpandCon : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pred.unexpandTest : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pol.unexpandFilter : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pol.unexpandDup : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pol.unexpandSeq : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pol.unexpandMod : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pol.unexpandAdd : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pol.unexpandWeight : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.Pol.unexpandIter : Lean.PrettyPrinter.Unexpander

Equations

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

def WeightedNetKAT.cwnk_pred.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer

Equations

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

def WeightedNetKAT.cwnk_pol.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer

Equations

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