inductive spGCL : Type

• skip : spGCL
• assign (v : HeyLo.Ident) : HeyLo v.type → spGCL
• seq : spGCL → spGCL → spGCL
• prob : spGCL → HeyLo HeyLo.Ty.ENNReal → spGCL → spGCL
• nonDet : spGCL → spGCL → spGCL
• ite : HeyLo HeyLo.Ty.Bool → spGCL → spGCL → spGCL
• loop : HeyLo HeyLo.Ty.Bool → HeyLo HeyLo.Ty.ENNReal → spGCL → spGCL
• tick : HeyLo HeyLo.Ty.ENNReal → spGCL
• observe : HeyLo HeyLo.Ty.Bool → spGCL

def instInhabitedSpGCL.default : spGCL

Equations

• instInhabitedSpGCL.default = spGCL.skip

@[implicit_reducible]

instance instInhabitedSpGCL : Inhabited spGCL

Equations

• instInhabitedSpGCL = { default := instInhabitedSpGCL.default }

noncomputable def spGCL.pGCL : spGCL → _root_.pGCL fun (x : HeyLo.Ident) => x.type.lit

Equations

• spGCL.skip.pGCL = pgcl {skip}
• (spGCL.assign x_1 e).pGCL = pgcl {@x_1 := @e.sem}
• (C₁.seq C₂).pGCL = pgcl {@C₁.pGCL ; @C₂.pGCL}
• (C₁.prob p C₂).pGCL = pgcl {{ @C₁.pGCL } [@(pGCL.ProbExp.ofExp p.sem)] { @C₂.pGCL }}
• (C₁.nonDet C₂).pGCL = pgcl {{ @C₁.pGCL } [] { @C₂.pGCL }}
• (spGCL.ite b C₁ C₂).pGCL = pgcl {if @fun (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) => b.sem σ then @C₁.pGCL else @C₂.pGCL end}
• (spGCL.loop b a C).pGCL = pgcl {while @fun (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) => b.sem σ { @C.pGCL }}
• (spGCL.tick r).pGCL = pgcl {tick(@r.sem)}
• (spGCL.observe b).pGCL = pgcl {observe(@fun (σ : pGCL.State fun (x : HeyLo.Ident) => x.type.lit) => b.sem σ)}