def MonoidModule (M : Type u_12) (A : Type u_13) [Monoid M] [AddMonoid A] : Type (max u_12 u_13)

Alias of DistribMulAction.

---

Typeclass for multiplicative actions on additive structures. This generalizes group modules.

Equations

• MonoidModule = DistribMulAction

def «term_⊙_» : Lean.TrailingParserDescr

a * b computes the product of a and b. The meaning of this notation is type-dependent.

Equations

• «term_⊙_» = Lean.ParserDescr.trailingNode `«term_⊙_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊙ ") (Lean.ParserDescr.cat `term 73))

def «term_⊗_» : Lean.TrailingParserDescr

a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

Equations

• «term_⊗_» = Lean.ParserDescr.trailingNode `«term_⊗_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 71))

@[reducible, inline]

abbrev 𝕎 (M Var : Type) : Type

Equations

• 𝕎 M Var = (Var → M)

instance Pi.instDistribMulAction (W M : Type) [Monoid W] [AddCommMonoid M] [DistribMulAction W M] {ι : Type u_1} : DistribMulAction W (ι → M)

Equations

• Pi.instDistribMulAction W M = { toMulAction := Pi.mulAction W, smul_zero := ⋯, smul_add := ⋯ }

instance instDistribMulAction𝕎 (W M : Type) [Monoid W] [AddCommMonoid M] [DistribMulAction W M] (Var : Type) : DistribMulAction W (𝕎 M Var)

Equations

• instDistribMulAction𝕎 W M Var = Pi.instDistribMulAction W M

instance instDistribMulAction_wGCL {𝒮 : Type} [inst : Semiring 𝒮] : DistribMulAction 𝒮 𝒮

Equations

• instDistribMulAction_wGCL = { toMulAction := DistribMulAction.toMulAction, smul_zero := ⋯, smul_add := ⋯ }

class OmegaCompleteSemiring (𝒮 : Type) [TopologicalSpace 𝒮] extends Semiring 𝒮 : Type

• add : 𝒮 → 𝒮 → 𝒮
• add_assoc (a b c : 𝒮) : a + b + c = a + (b + c)
• zero : 𝒮
• zero_add (a : 𝒮) : 0 + a = a
• add_zero (a : 𝒮) : a + 0 = a
• nsmul : ℕ → 𝒮 → 𝒮
• nsmul_zero (x : 𝒮) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : 𝒮) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : 𝒮) : a + b = b + a
• mul : 𝒮 → 𝒮 → 𝒮
• left_distrib (a b c : 𝒮) : a ⊙ (b + c) = a ⊙ b + a ⊙ c
• right_distrib (a b c : 𝒮) : (a + b) ⊙ c = a ⊙ c + b ⊙ c
• zero_mul (a : 𝒮) : 0 ⊙ a = 0
• mul_zero (a : 𝒮) : a ⊙ 0 = 0
• mul_assoc (a b c : 𝒮) : (a ⊙ b) ⊙ c = a ⊙ b ⊙ c
• one : 𝒮
• one_mul (a : 𝒮) : 1 ⊙ a = a
• mul_one (a : 𝒮) : a ⊙ 1 = a
• natCast : ℕ → 𝒮
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → 𝒮 → 𝒮
• npow_zero (x : 𝒮) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : 𝒮) : Semiring.npow (n + 1) x = Semiring.npow n x ⊙ x
• sum_mul_left {ι : Type u_1} {f : ι → 𝒮} {a : 𝒮} : ∑' (x : ι), a ⊙ f x = a ⊙ ∑' (x : ι), f x
• sum_mul_right {ι : Type u_2} {f : ι → 𝒮} {a : 𝒮} : ∑' (x : ι), f x ⊙ a = (∑' (x : ι), f x) ⊙ a
• sum_biUnion {ι : Type u_3} {α : Type u_4} {S : Set ι} {f : α → 𝒮} {t : ι → Set α} (h : S.PairwiseDisjoint t) : ∑' (x : ↑(⋃ i ∈ S, t i)), f ↑x = ∑' (i : ↑S) (x : ↑(t ↑i)), f ↑x

def WGCL.Mem (D Var : Type) : Type

Equations

• WGCL.Mem D Var = (Var → D)

@[reducible, inline]

abbrev WGCL.Weighting (D M Var : Type) : Type

Equations

• WGCL.Weighting D M Var = 𝕎 M (WGCL.Mem D Var)

@[reducible, inline]

abbrev WGCL.AExpr (D Var : Type) : Type

Equations

• WGCL.AExpr D Var = (WGCL.Mem D Var → D)

@[reducible, inline]

abbrev WGCL.BExpr (D Var : Type) : Type

Equations

• WGCL.BExpr D Var = (WGCL.Mem D Var → Prop)

inductive WGCL.wGCL (D W Var : Type) : Type

• Branch {D W Var : Type} : wGCL D W Var → wGCL D W Var → wGCL D W Var
• Weight {D W Var : Type} : 𝕎 W (Mem D Var) → wGCL D W Var
• Assign {D W Var : Type} : Var → AExpr D Var → wGCL D W Var
• Ite {D W Var : Type} : BExpr D Var → wGCL D W Var → wGCL D W Var → wGCL D W Var
• Seq {D W Var : Type} : wGCL D W Var → wGCL D W Var → wGCL D W Var
• While {D W Var : Type} : BExpr D Var → wGCL D W Var → wGCL D W Var

def Lean.Parser.Category.cwgcl_var : Category

Equations

• Lean.Parser.Category.cwgcl_var = { }

def WGCL.cwgcl_var.quot : Lean.ParserDescr

Equations

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

def WGCL.«termWgcl_var{_}» : Lean.ParserDescr

Equations

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

def WGCL.cwgcl_bexp.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwgcl_bexp : Category

Equations

• Lean.Parser.Category.cwgcl_bexp = { }

def WGCL.«termWgcl_bexp{_}» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwgcl_aexp : Category

Equations

• Lean.Parser.Category.cwgcl_aexp = { }

def WGCL.cwgcl_aexp.quot : Lean.ParserDescr

Equations

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

def WGCL.«termWgcl_aexp{_}» : Lean.ParserDescr

Equations

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

def WGCL.cwgcl_wght.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwgcl_wght : Category

Equations

• Lean.Parser.Category.cwgcl_wght = { }

def WGCL.«termWght{_}» : Lean.ParserDescr

Equations

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

def WGCL.cwgcl_prog.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cwgcl_prog : Category

Equations

• Lean.Parser.Category.cwgcl_prog = { }

def WGCL.«termWgcl_{_}» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_var~_» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_bexp~_» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_aexp~_» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_wght~_» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_prog~_» : Lean.ParserDescr

Equations

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

def WGCL.cwgcl_var_ : Lean.ParserDescr

Equations

• WGCL.cwgcl_var_ = Lean.ParserDescr.node `WGCL.cwgcl_var_ 1022 (Lean.ParserDescr.const `ident)

def WGCL.cwgcl_bexp_ : Lean.ParserDescr

Equations

• WGCL.cwgcl_bexp_ = Lean.ParserDescr.node `WGCL.cwgcl_bexp_ 1022 (Lean.ParserDescr.const `ident)

def WGCL.cwgcl_aexp_ : Lean.ParserDescr

Equations

• WGCL.cwgcl_aexp_ = Lean.ParserDescr.node `WGCL.cwgcl_aexp_ 1022 (Lean.ParserDescr.const `num)

def WGCL.«cwgcl_aexp_+_» : Lean.TrailingParserDescr

Equations

• WGCL.«cwgcl_aexp_+_» = Lean.ParserDescr.trailingNode `WGCL.«cwgcl_aexp_+_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `cwgcl_aexp 51))

def WGCL.cwgcl_wght_ : Lean.ParserDescr

Equations

• WGCL.cwgcl_wght_ = Lean.ParserDescr.node `WGCL.cwgcl_wght_ 1022 (Lean.ParserDescr.const `num)

def WGCL.cwgcl_wght__1 : Lean.ParserDescr

Equations

• WGCL.cwgcl_wght__1 = Lean.ParserDescr.node `WGCL.cwgcl_wght__1 1022 (Lean.ParserDescr.const `ident)

def WGCL.«cwgcl_prog⊙_» : Lean.ParserDescr

Equations

• WGCL.«cwgcl_prog⊙_» = Lean.ParserDescr.node `WGCL.«cwgcl_prog⊙_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊙") (Lean.ParserDescr.cat `cwgcl_wght 0))

def WGCL.«cwgcl_prog__:=__» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_prog{_}⊕{_}» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_prog_;__» : Lean.TrailingParserDescr

Equations

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

def WGCL.«cwgcl_progIf(_)_{___}_Else_{___}» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_progIf(_)_{___}» : Lean.ParserDescr

Equations

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

def WGCL.«cwgcl_progWhile(_)_{___}» : Lean.ParserDescr

Equations

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

def WGCL.cwgcl_progSkip : Lean.ParserDescr

Equations

• WGCL.cwgcl_progSkip = Lean.ParserDescr.node `WGCL.cwgcl_progSkip 1024 (Lean.ParserDescr.symbol "skip")

def WGCL.unexpandWeighting : Lean.TSyntax `term → Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `cwgcl_wght)

Equations

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

def WGCL.wGCL.unexpandWeight : Lean.PrettyPrinter.Unexpander

Equations

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

def WGCL.wGCL.unexpandBranch : Lean.PrettyPrinter.Unexpander

Equations

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

def WGCL.wGCL.unexpandSeq : Lean.PrettyPrinter.Unexpander

Equations

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

def WGCL.wGCL.unexpandBExpr : Lean.TSyntax `term → Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `cwgcl_bexp)

Equations

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

partial def WGCL.wGCL.unexpandAExpr : Lean.TSyntax `term → Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `cwgcl_aexp)

def WGCL.wGCL.unexpandIte : Lean.PrettyPrinter.Unexpander

Equations

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

def WGCL.wGCL.unexpandWhile : Lean.PrettyPrinter.Unexpander

Equations

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

def WGCL.wGCL.unexpandAssign : Lean.PrettyPrinter.Unexpander

Equations

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