inductive pGCL (ϖ : Type u_2) : Type u_2

• skip {ϖ : Type u_2} : pGCL ϖ
• assign {ϖ : Type u_2} : ϖ → Exp ϖ → pGCL ϖ
• seq {ϖ : Type u_2} : pGCL ϖ → pGCL ϖ → pGCL ϖ
• prob {ϖ : Type u_2} : pGCL ϖ → ProbExp ϖ → pGCL ϖ → pGCL ϖ
• nonDet {ϖ : Type u_2} : pGCL ϖ → pGCL ϖ → pGCL ϖ
• loop {ϖ : Type u_2} : BExpr ϖ → pGCL ϖ → pGCL ϖ
• tick {ϖ : Type u_2} : Exp ϖ → pGCL ϖ

instance instInhabitedPGCL {a✝ : Type u_2} : Inhabited (pGCL a✝)

Equations

• instInhabitedPGCL = { default := pGCL.skip }

noncomputable instance pGCL.decidableEq {ϖ : Type u_1} [DecidableEq ϖ] : DecidableEq (pGCL ϖ)

Equations

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

def «term_;;_» : Lean.TrailingParserDescr

Equations

• «term_;;_» = Lean.ParserDescr.trailingNode `«term_;;_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ;; ") (Lean.ParserDescr.cat `term 90))

def «term_·[]_» : Lean.TrailingParserDescr

Equations

• «term_·[]_» = Lean.ParserDescr.trailingNode `«term_·[]_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ·[] ") (Lean.ParserDescr.cat `term 90))

def «term_::=_» : Lean.TrailingParserDescr

Equations

• «term_::=_» = Lean.ParserDescr.trailingNode `«term_::=_» 91 92 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::= ") (Lean.ParserDescr.cat `term 91))

def «term_·[_]_» : Lean.TrailingParserDescr

Equations

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