def HeyVL.vp (C : HeyVL) (φ : HeyLo HeyLo.Ty.ENNReal) : HeyLo HeyLo.Ty.ENNReal

Equations

• (vp⟦x :≈ @μ⟧) φ = (μ.map fun (v : HeyLo x.type) => φ[x ↦ v]).toExpr
• vp⟦reward(@a)⟧ φ = φ + a
• (vp⟦@S₁ ; @S₂⟧) φ = vp⟦@S₁⟧ (vp⟦@S₂⟧ φ)
• vp⟦if (⊓) {@S₁} else {@S₂}⟧ φ = vp⟦@S₁⟧ φ ⊓ vp⟦@S₂⟧ φ
• vp⟦assert(@ψ)⟧ φ = ψ ⊓ φ
• vp⟦assume(@ψ)⟧ φ = ψ ⇨ φ
• vp⟦havoc(@x)⟧ φ = HeyLo.Quant HeyLo.QuantOp.Inf x φ
• (vp⟦validate⟧) φ = ￢￢φ
• vp⟦if (⊔) {@S₁} else {@S₂}⟧ φ = vp⟦@S₁⟧ φ ⊔ vp⟦@S₂⟧ φ
• vp⟦coassert(@ψ)⟧ φ = ψ ⊔ φ
• vp⟦coassume(@ψ)⟧ φ = φ \ ψ
• vp⟦cohavoc(@x)⟧ φ = HeyLo.Quant HeyLo.QuantOp.Sup x φ
• (vp⟦covalidate⟧) φ = ~ ~ φ

def «termVp⟦_⟧» : Lean.ParserDescr

Equations

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

def «termVp⟦_⟧(_)» : Lean.ParserDescr

Equations

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

def vpUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

@[reducible, inline]

abbrev HeyVL.vp.example.x : HeyLo.Ident

Equations

• HeyVL.vp.example.x = { name := "x", type := HeyLo.Ty.Bool }

@[simp]

theorem HeyVL.fv_vp {φ : HeyLo HeyLo.Ty.ENNReal} {P : HeyVL} : (vp⟦@P⟧ φ).fv = P.fv ∪ φ.fv