inductive HeyVL : Type

• Assign (x : HeyLo.Ident) (μ : HeyLo.Distribution x.type) : HeyVL

  x :≈ μ

• Reward (a : HeyLo HeyLo.Ty.ENNReal) : HeyVL

  reward μ

• Seq (S₁ S₂ : HeyVL) : HeyVL

  S₁ ; S₂

• IfInf (S₁ S₂ : HeyVL) : HeyVL

  if (⊓) { S₁ } else { S₂ }

• Assert (φ : HeyLo HeyLo.Ty.ENNReal) : HeyVL

  assert φ

• Assume (φ : HeyLo HeyLo.Ty.ENNReal) : HeyVL

  assume φ

• Havoc (x : HeyLo.Ident) : HeyVL

  havoc x

• Validate : HeyVL

  validate

• IfSup (S₁ S₂ : HeyVL) : HeyVL

  if (⊔) { S₁ } else { S₂ }

• Coassert (φ : HeyLo HeyLo.Ty.ENNReal) : HeyVL

  coassert φ

• Coassume (φ : HeyLo HeyLo.Ty.ENNReal) : HeyVL

  coassume φ

• Cohavoc (x : HeyLo.Ident) : HeyVL

  cohavoc x

• Covalidate : HeyVL

  covalidate

def instToExprHeyVL.toExpr : HeyVL → Lean.Expr

Equations

• instToExprHeyVL.toExpr (HeyVL.Assign a a_1) = ((Lean.Expr.const `HeyVL.Assign []).app (Lean.toExpr a)).app (Lean.toExpr a_1)
• instToExprHeyVL.toExpr (HeyVL.Reward a) = (Lean.Expr.const `HeyVL.Reward []).app (Lean.toExpr a)
• instToExprHeyVL.toExpr (a ;; a_1) = ((Lean.Expr.const `HeyVL.Seq []).app (instToExprHeyVL.toExpr a)).app (instToExprHeyVL.toExpr a_1)
• instToExprHeyVL.toExpr (a.IfInf a_1) = ((Lean.Expr.const `HeyVL.IfInf []).app (instToExprHeyVL.toExpr a)).app (instToExprHeyVL.toExpr a_1)
• instToExprHeyVL.toExpr (HeyVL.Assert a) = (Lean.Expr.const `HeyVL.Assert []).app (Lean.toExpr a)
• instToExprHeyVL.toExpr (HeyVL.Assume a) = (Lean.Expr.const `HeyVL.Assume []).app (Lean.toExpr a)
• instToExprHeyVL.toExpr (HeyVL.Havoc a) = (Lean.Expr.const `HeyVL.Havoc []).app (Lean.toExpr a)
• instToExprHeyVL.toExpr HeyVL.Validate = Lean.Expr.const `HeyVL.Validate []
• instToExprHeyVL.toExpr (a.IfSup a_1) = ((Lean.Expr.const `HeyVL.IfSup []).app (instToExprHeyVL.toExpr a)).app (instToExprHeyVL.toExpr a_1)
• instToExprHeyVL.toExpr (HeyVL.Coassert a) = (Lean.Expr.const `HeyVL.Coassert []).app (Lean.toExpr a)
• instToExprHeyVL.toExpr (HeyVL.Coassume a) = (Lean.Expr.const `HeyVL.Coassume []).app (Lean.toExpr a)
• instToExprHeyVL.toExpr (HeyVL.Cohavoc a) = (Lean.Expr.const `HeyVL.Cohavoc []).app (Lean.toExpr a)
• instToExprHeyVL.toExpr HeyVL.Covalidate = Lean.Expr.const `HeyVL.Covalidate []

@[implicit_reducible]

instance instToExprHeyVL : Lean.ToExpr HeyVL

Equations

• instToExprHeyVL = { toExpr := instToExprHeyVL.toExpr, toTypeExpr := Lean.Expr.const `HeyVL [] }

def instDecidableEqHeyVL.decEq (x✝ x✝¹ : HeyVL) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqHeyVL : DecidableEq HeyVL

Equations

• instDecidableEqHeyVL = instDecidableEqHeyVL.decEq

def «term_;;_» : Lean.TrailingParserDescr

Equations

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

def HeyVL.Skip : HeyVL

Equations

• HeyVL.Skip = HeyVL.Reward 0

def HeyVL.If (b : HeyLo HeyLo.Ty.Bool) (S₁ S₂ : HeyVL) : HeyVL

Equations

• HeyVL.If b S₁ S₂ = (HeyVL.Assume b.embed ;; S₁).IfInf (HeyVL.Assume b.not.embed ;; S₂)

def HeyVL.Havocs (xs : List HeyLo.Ident) : HeyVL

Equations

• HeyVL.Havocs [] = HeyVL.Skip
• HeyVL.Havocs [x] = HeyVL.Havoc x
• HeyVL.Havocs (x :: xs_2) = (HeyVL.Havoc x ;; HeyVL.Havocs xs_2)

def HeyVL.Cohavocs (xs : List HeyLo.Ident) : HeyVL

Equations

• HeyVL.Cohavocs [] = HeyVL.Skip
• HeyVL.Cohavocs [x] = HeyVL.Cohavoc x
• HeyVL.Cohavocs (x :: xs_2) = (HeyVL.Cohavoc x ;; HeyVL.Cohavocs xs_2)