inductive pGCL {𝒱 : Type u_1} (Γ : 𝒱 → Type u_3) : Type (max u_1 u_3)

• skip {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} : pGCL Γ
• assign {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} (v : 𝒱) : (State Γ → Γ v) → pGCL Γ
• seq {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} : pGCL Γ → pGCL Γ → pGCL Γ
• prob {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} : pGCL Γ → ProbExp Γ → pGCL Γ → pGCL Γ
• nonDet {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} : pGCL Γ → pGCL Γ → pGCL Γ
• loop {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} : (State Γ → Prop) → pGCL Γ → pGCL Γ
• tick {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} : (State Γ → ENNReal) → pGCL Γ
• observe {𝒱 : Type u_1} {Γ : 𝒱 → Type u_3} : (State Γ → Prop) → pGCL Γ

def instInhabitedPGCL.default {a✝ : Type u_3} {a✝¹ : a✝ → Type u_4} : pGCL a✝¹

Equations

• instInhabitedPGCL.default = pgcl {skip}

instance instInhabitedPGCL {a✝ : Type u_3} {a✝¹ : a✝ → Type u_4} : Inhabited (pGCL a✝¹)

Equations

• instInhabitedPGCL = { default := instInhabitedPGCL.default }

noncomputable def pGCL.ite {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (b : BExpr Γ) (C₁ C₂ : pGCL Γ) : pGCL Γ

Equations

• pgcl {if @b then @C₁ else @C₂ end} = pgcl {{ @C₁ } [@p[b]] { @C₂ }}

noncomputable instance pGCL.decidableEq {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} [DecidableEq 𝒱] : DecidableEq (pGCL Γ)

Equations

• x✝¹.decidableEq x✝ = Classical.propDecidable (x✝¹ = x✝)

def pGCL.cpgcl_var.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cpgcl_var : Category

Equations

• Lean.Parser.Category.cpgcl_var = { }

def pGCL.«termPgcl_var{_}» : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cpgcl_bexp : Category

Equations

• Lean.Parser.Category.cpgcl_bexp = { }

def pGCL.cpgcl_bexp.quot : Lean.ParserDescr

Equations

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

def pGCL.«termPgcl_bexp{_}» : Lean.ParserDescr

Equations

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

def pGCL.cpgcl_aexp.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cpgcl_aexp : Category

Equations

• Lean.Parser.Category.cpgcl_aexp = { }

def pGCL.«termPgcl_aexp{_}» : Lean.ParserDescr

Equations

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

def pGCL.cpgcl_pexp.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cpgcl_pexp : Category

Equations

• Lean.Parser.Category.cpgcl_pexp = { }

def pGCL.«termPgcl_pexp{_}» : Lean.ParserDescr

Equations

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

def pGCL.cpgcl_prog.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cpgcl_prog : Category

Equations

• Lean.Parser.Category.cpgcl_prog = { }

def pGCL.«termPgcl_{_}» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_var@_» : Lean.ParserDescr

Equations

• pGCL.«cpgcl_var@_» = Lean.ParserDescr.node `pGCL.«cpgcl_var@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def pGCL.«cpgcl_bexp@_» : Lean.ParserDescr

Equations

• pGCL.«cpgcl_bexp@_» = Lean.ParserDescr.node `pGCL.«cpgcl_bexp@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def pGCL.«cpgcl_aexp@_» : Lean.ParserDescr

Equations

• pGCL.«cpgcl_aexp@_» = Lean.ParserDescr.node `pGCL.«cpgcl_aexp@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def pGCL.«cpgcl_pexp@_» : Lean.ParserDescr

Equations

• pGCL.«cpgcl_pexp@_» = Lean.ParserDescr.node `pGCL.«cpgcl_pexp@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def pGCL.«cpgcl_prog@_» : Lean.ParserDescr

Equations

• pGCL.«cpgcl_prog@_» = Lean.ParserDescr.node `pGCL.«cpgcl_prog@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def pGCL.cpgcl_var_ : Lean.ParserDescr

Equations

• pGCL.cpgcl_var_ = Lean.ParserDescr.node `pGCL.cpgcl_var_ 1022 (Lean.ParserDescr.const `ident)

def pGCL.cpgcl_aexp_ : Lean.ParserDescr

Equations

• pGCL.cpgcl_aexp_ = Lean.ParserDescr.node `pGCL.cpgcl_aexp_ 1022 (Lean.ParserDescr.const `num)

def pGCL.cpgcl_aexp__1 : Lean.ParserDescr

Equations

• pGCL.cpgcl_aexp__1 = Lean.ParserDescr.node `pGCL.cpgcl_aexp__1 1022 (Lean.ParserDescr.const `ident)

def pGCL.«cpgcl_aexp_+_» : Lean.TrailingParserDescr

Equations

• pGCL.«cpgcl_aexp_+_» = Lean.ParserDescr.trailingNode `pGCL.«cpgcl_aexp_+_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `cpgcl_aexp 0))

def pGCL.«cpgcl_aexp_-_» : Lean.TrailingParserDescr

Equations

• pGCL.«cpgcl_aexp_-_» = Lean.ParserDescr.trailingNode `pGCL.«cpgcl_aexp_-_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `cpgcl_aexp 0))

def pGCL.«cpgcl_aexp_*_» : Lean.TrailingParserDescr

Equations

• pGCL.«cpgcl_aexp_*_» = Lean.ParserDescr.trailingNode `pGCL.«cpgcl_aexp_*_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " * ") (Lean.ParserDescr.cat `cpgcl_aexp 0))

def pGCL.«cpgcl_aexp_/_» : Lean.TrailingParserDescr

Equations

• pGCL.«cpgcl_aexp_/_» = Lean.ParserDescr.trailingNode `pGCL.«cpgcl_aexp_/_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " / ") (Lean.ParserDescr.cat `cpgcl_aexp 0))

def pGCL.«cpgcl_aexp[_]» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_aexp(_)» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_pexp_⁻¹» : Lean.ParserDescr

Equations

• pGCL.«cpgcl_pexp_⁻¹» = Lean.ParserDescr.node `pGCL.«cpgcl_pexp_⁻¹» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat `cpgcl_aexp 0) (Lean.ParserDescr.symbol "⁻¹"))

def pGCL.cpgcl_bexp_ : Lean.ParserDescr

Equations

• pGCL.cpgcl_bexp_ = Lean.ParserDescr.node `pGCL.cpgcl_bexp_ 1022 (Lean.ParserDescr.const `ident)

def pGCL.«cpgcl_bexp_<_» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_bexp_≤_» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_bexp_=_» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_bexp_∧_» : Lean.TrailingParserDescr

Equations

• pGCL.«cpgcl_bexp_∧_» = Lean.ParserDescr.trailingNode `pGCL.«cpgcl_bexp_∧_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `cpgcl_bexp 0))

def pGCL.«cpgcl_bexp_∨_» : Lean.TrailingParserDescr

Equations

• pGCL.«cpgcl_bexp_∨_» = Lean.ParserDescr.trailingNode `pGCL.«cpgcl_bexp_∨_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `cpgcl_bexp 0))

def pGCL.«cpgcl_bexp¬_» : Lean.ParserDescr

Equations

• pGCL.«cpgcl_bexp¬_» = Lean.ParserDescr.node `pGCL.«cpgcl_bexp¬_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `cpgcl_bexp 0))

def pGCL.«cpgcl_bexp(_)» : Lean.ParserDescr

Equations

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

def pGCL.cpgcl_prog_ : Lean.ParserDescr

Equations

• pGCL.cpgcl_prog_ = Lean.ParserDescr.node `pGCL.cpgcl_prog_ 1022 (Lean.ParserDescr.const `ident)

def pGCL.«cpgcl_prog_:=_» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_prog_;_» : Lean.TrailingParserDescr

Equations

• pGCL.«cpgcl_prog_;_» = Lean.ParserDescr.trailingNode `pGCL.«cpgcl_prog_;_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ; ") (Lean.ParserDescr.cat `cpgcl_prog 0))

def pGCL.«cpgcl_prog{_}[_]{_}» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_prog{_}[]{_}» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_progWhile_{_}» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_progTick(_)» : Lean.ParserDescr

Equations

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

def pGCL.«cpgcl_progObserve(_)» : Lean.ParserDescr

Equations

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

def pGCL.cpgcl_progIf_Then_Else_End : Lean.ParserDescr

Equations

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

def pGCL.Exp.const {𝒱 : Type u_1} {Γ : 𝒱 → Type u_2} (c : 𝒱) : State Γ → Γ c

Equations

• pGCL.Exp.const c x✝ = x✝ c

partial def pGCL.unexpandAexp : Lean.TSyntax `term → Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `cpgcl_aexp)

def pGCL.unexpandBExp : Lean.TSyntax `term → Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `cpgcl_bexp)

Equations

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

def pGCL.BExpr.eqUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.probExpUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.skipUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.assignUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.seqUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.probUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.nonDetUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.loopUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.tickUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.observeUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def pGCL.iteUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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