inductive HeyLo.Ty : Type

• Bool : Ty
• Nat : Ty
• ENNReal : Ty

@[implicit_reducible]

instance HeyLo.instToExprTy : Lean.ToExpr Ty

Equations

• HeyLo.instToExprTy = { toExpr := HeyLo.instToExprTy.toExpr, toTypeExpr := Lean.Expr.const `HeyLo.Ty [] }

def HeyLo.instToExprTy.toExpr : Ty → Lean.Expr

Equations

• HeyLo.instToExprTy.toExpr HeyLo.Ty.Bool = Lean.Expr.const `HeyLo.Ty.Bool []
• HeyLo.instToExprTy.toExpr HeyLo.Ty.Nat = Lean.Expr.const `HeyLo.Ty.Nat []
• HeyLo.instToExprTy.toExpr HeyLo.Ty.ENNReal = Lean.Expr.const `HeyLo.Ty.ENNReal []

@[implicit_reducible]

instance HeyLo.instDecidableEqTy : DecidableEq Ty

Equations

• HeyLo.instDecidableEqTy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HeyLo.instHashableTy : Hashable Ty

Equations

• HeyLo.instHashableTy = { hash := HeyLo.instHashableTy.hash }

def HeyLo.instHashableTy.hash : Ty → UInt64

Equations

• HeyLo.instHashableTy.hash HeyLo.Ty.Bool = 0
• HeyLo.instHashableTy.hash HeyLo.Ty.Nat = 1
• HeyLo.instHashableTy.hash HeyLo.Ty.ENNReal = 2

def HeyLo.instInhabitedTy.default : Ty

Equations

• HeyLo.instInhabitedTy.default = HeyLo.Ty.Bool

@[implicit_reducible]

instance HeyLo.instInhabitedTy : Inhabited Ty

Equations

• HeyLo.instInhabitedTy = { default := HeyLo.instInhabitedTy.default }

def HeyLo.Ty.toNat : Ty → ℕ

Equations

• HeyLo.Ty.Bool.toNat = 0
• HeyLo.Ty.Nat.toNat = 1
• HeyLo.Ty.ENNReal.toNat = 2

@[implicit_reducible]

instance HeyLo.Ty.instLinearOrder : LinearOrder Ty

Equations

• HeyLo.Ty.instLinearOrder = LinearOrder.lift' HeyLo.Ty.toNat ⋯

@[reducible, inline]

abbrev HeyLo.Ty.lit : Ty → Type

Equations

• HeyLo.Ty.Bool.lit = Prop
• HeyLo.Ty.ENNReal.lit = ENNReal
• HeyLo.Ty.Nat.lit = ℕ

inductive HeyLo.Yes : Type

• yes : Yes

def HeyLo.instToExprYes.toExpr : Yes → Lean.Expr

Equations

• HeyLo.instToExprYes.toExpr HeyLo.Yes.yes = Lean.Expr.const `HeyLo.Yes.yes []

@[implicit_reducible]

instance HeyLo.instToExprYes : Lean.ToExpr Yes

Equations

• HeyLo.instToExprYes = { toExpr := HeyLo.instToExprYes.toExpr, toTypeExpr := Lean.Expr.const `HeyLo.Yes [] }

@[implicit_reducible]

instance HeyLo.instDecidableEqYes : DecidableEq Yes

Equations

• HeyLo.instDecidableEqYes x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HeyLo.instHashableYes.hash : Yes → UInt64

Equations

• HeyLo.instHashableYes.hash HeyLo.Yes.yes = 0

@[implicit_reducible]

instance HeyLo.instHashableYes : Hashable Yes

Equations

• HeyLo.instHashableYes = { hash := HeyLo.instHashableYes.hash }

def HeyLo.instInhabitedYes.default : Yes

Equations

• HeyLo.instInhabitedYes.default = HeyLo.Yes.yes

@[implicit_reducible]

instance HeyLo.instInhabitedYes : Inhabited Yes

Equations

• HeyLo.instInhabitedYes = { default := HeyLo.instInhabitedYes.default }

inductive HeyLo.No : Type

@[implicit_reducible]

instance HeyLo.instToExprNo : Lean.ToExpr No

Equations

• HeyLo.instToExprNo = { toExpr := HeyLo.instToExprNo.toExpr, toTypeExpr := Lean.Expr.const `HeyLo.No [] }

def HeyLo.instToExprNo.toExpr : No → Lean.Expr

def HeyLo.instDecidableEqNo.decEq (x✝ x✝¹ : No) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance HeyLo.instDecidableEqNo : DecidableEq No

Equations

• HeyLo.instDecidableEqNo = HeyLo.instDecidableEqNo.decEq

def HeyLo.instHashableNo.hash : No → UInt64

@[implicit_reducible]

instance HeyLo.instHashableNo : Hashable No

Equations

• HeyLo.instHashableNo = { hash := HeyLo.instHashableNo.hash }

@[reducible, inline]

abbrev HeyLo.Ty.Compare : Ty → Type

Equations

• HeyLo.Ty.Bool.Compare = HeyLo.No
• HeyLo.Ty.ENNReal.Compare = HeyLo.Yes
• HeyLo.Ty.Nat.Compare = HeyLo.Yes

@[reducible, inline]

abbrev HeyLo.Ty.Arith : Ty → Type

Equations

• HeyLo.Ty.Bool.Arith = HeyLo.No
• HeyLo.Ty.ENNReal.Arith = HeyLo.Yes
• HeyLo.Ty.Nat.Arith = HeyLo.Yes

@[implicit_reducible]

instance HeyLo.instToExprCompare {α : Ty} : Lean.ToExpr α.Compare

Equations

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

@[implicit_reducible]

instance HeyLo.instToExprArith {α : Ty} : Lean.ToExpr α.Arith

Equations

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

@[implicit_reducible]

instance HeyLo.instDecidableEqCompare {α : Ty} : DecidableEq α.Compare

Equations

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

@[implicit_reducible]

instance HeyLo.instDecidableEqArith {α : Ty} : DecidableEq α.Arith

Equations

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

inductive HeyLo.BinOp : Ty → Ty → Type

• Add {α : Ty} : α.Arith → BinOp α α

  The + operator (addition).

• Sub {α : Ty} : α.Arith → BinOp α α

  The - operator (subtraction).

• Mul {α : Ty} : α.Arith → BinOp α α

  The * operator (multiplication).

• Div {α : Ty} : α.Arith → BinOp α α

  The / operator (division).

• Mod : BinOp Ty.Nat Ty.Nat

  The % operator (modulo).

• And : BinOp Ty.Bool Ty.Bool

  The && operator (logical and).

• Or : BinOp Ty.Bool Ty.Bool

  The || operator (logical or).

• Eq {α : Ty} : BinOp α Ty.Bool

  The == operator (equality).

• Lt {α : Ty} : α.Compare → BinOp α Ty.Bool

  The < operator (less than).

• Le {α : Ty} : α.Compare → BinOp α Ty.Bool

  The <= operator (less than or equal to).

• Ne {α : Ty} : α.Compare → BinOp α Ty.Bool

  The != operator (not equal to).

• Ge {α : Ty} : α.Compare → BinOp α Ty.Bool

  The >= operator (greater than or equal to).

• Gt {α : Ty} : α.Compare → BinOp α Ty.Bool

  The > operator (greater than).

• Inf : BinOp Ty.ENNReal Ty.ENNReal

  The ⊓ operator (infimum).

• Sup : BinOp Ty.ENNReal Ty.ENNReal

  The ⊔ operator (supremum).

• Impl : BinOp Ty.ENNReal Ty.ENNReal

  The → operator (implication).

• CoImpl : BinOp Ty.ENNReal Ty.ENNReal

  The ← operator (co-implication).

def HeyLo.instToExprBinOp.toExpr {a✝ a✝¹ : Ty} : BinOp a✝ a✝¹ → Lean.Expr

Equations

• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Add a_3) = ((Lean.Expr.const `HeyLo.BinOp.Add []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Sub a_3) = ((Lean.Expr.const `HeyLo.BinOp.Sub []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Mul a_3) = ((Lean.Expr.const `HeyLo.BinOp.Mul []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Div a_3) = ((Lean.Expr.const `HeyLo.BinOp.Div []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.Mod = Lean.Expr.const `HeyLo.BinOp.Mod []
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.And = Lean.Expr.const `HeyLo.BinOp.And []
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.Or = Lean.Expr.const `HeyLo.BinOp.Or []
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.Eq = (Lean.Expr.const `HeyLo.BinOp.Eq []).app (Lean.toExpr a✝)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Lt a_3) = ((Lean.Expr.const `HeyLo.BinOp.Lt []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Le a_3) = ((Lean.Expr.const `HeyLo.BinOp.Le []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Ne a_3) = ((Lean.Expr.const `HeyLo.BinOp.Ne []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Ge a_3) = ((Lean.Expr.const `HeyLo.BinOp.Ge []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr (HeyLo.BinOp.Gt a_3) = ((Lean.Expr.const `HeyLo.BinOp.Gt []).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.Inf = Lean.Expr.const `HeyLo.BinOp.Inf []
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.Sup = Lean.Expr.const `HeyLo.BinOp.Sup []
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.Impl = Lean.Expr.const `HeyLo.BinOp.Impl []
• HeyLo.instToExprBinOp.toExpr HeyLo.BinOp.CoImpl = Lean.Expr.const `HeyLo.BinOp.CoImpl []

@[implicit_reducible]

instance HeyLo.instToExprBinOp {a✝ a✝¹ : Ty} : Lean.ToExpr (BinOp a✝ a✝¹)

Equations

• HeyLo.instToExprBinOp = { toExpr := HeyLo.instToExprBinOp.toExpr, toTypeExpr := ((Lean.Expr.const `HeyLo.BinOp []).app (Lean.toExpr a✝¹)).app (Lean.toExpr a✝) }

@[implicit_reducible]

instance HeyLo.instDecidableEqBinOp {a✝ a✝¹ : Ty} : DecidableEq (BinOp a✝ a✝¹)

Equations

• HeyLo.instDecidableEqBinOp = HeyLo.instDecidableEqBinOp.decEq

def HeyLo.instDecidableEqBinOp.decEq {a✝ a✝¹ : Ty} (x✝ x✝¹ : BinOp a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

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

inductive HeyLo.UnOp : Ty → Ty → Type

• Not {α : Ty} : UnOp α α

  The ! operator (negation).

• Non : UnOp Ty.ENNReal Ty.ENNReal

  The ~ operator (dual of negation),

• Embed : UnOp Ty.Bool Ty.ENNReal

  Boolean embedding (maps true to top in the lattice).

• Iverson : UnOp Ty.Bool Ty.ENNReal

  Iverson bracket (maps true to 1).

• NatToENNReal : UnOp Ty.Nat Ty.ENNReal

  Cast Nat to ENNReal

@[implicit_reducible]

instance HeyLo.instToExprUnOp {a✝ a✝¹ : Ty} : Lean.ToExpr (UnOp a✝ a✝¹)

Equations

• HeyLo.instToExprUnOp = { toExpr := HeyLo.instToExprUnOp.toExpr, toTypeExpr := ((Lean.Expr.const `HeyLo.UnOp []).app (Lean.toExpr a✝¹)).app (Lean.toExpr a✝) }

def HeyLo.instToExprUnOp.toExpr {a✝ a✝¹ : Ty} : UnOp a✝ a✝¹ → Lean.Expr

Equations

• HeyLo.instToExprUnOp.toExpr HeyLo.UnOp.Not = (Lean.Expr.const `HeyLo.UnOp.Not []).app (Lean.toExpr a✝)
• HeyLo.instToExprUnOp.toExpr HeyLo.UnOp.Non = Lean.Expr.const `HeyLo.UnOp.Non []
• HeyLo.instToExprUnOp.toExpr HeyLo.UnOp.Embed = Lean.Expr.const `HeyLo.UnOp.Embed []
• HeyLo.instToExprUnOp.toExpr HeyLo.UnOp.Iverson = Lean.Expr.const `HeyLo.UnOp.Iverson []
• HeyLo.instToExprUnOp.toExpr HeyLo.UnOp.NatToENNReal = Lean.Expr.const `HeyLo.UnOp.NatToENNReal []

def HeyLo.instDecidableEqUnOp.decEq {a✝ a✝¹ : Ty} (x✝ x✝¹ : UnOp a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Not HeyLo.UnOp.Not = isTrue ⋯
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Not HeyLo.UnOp.Non = isFalse HeyLo.instDecidableEqUnOp.decEq._proof_2
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Non HeyLo.UnOp.Not = isFalse HeyLo.instDecidableEqUnOp.decEq._proof_3
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Non HeyLo.UnOp.Non = isTrue HeyLo.instDecidableEqUnOp.decEq._proof_4
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Embed HeyLo.UnOp.Embed = isTrue HeyLo.instDecidableEqUnOp.decEq._proof_5
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Embed HeyLo.UnOp.Iverson = isFalse HeyLo.instDecidableEqUnOp.decEq._proof_6
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Iverson HeyLo.UnOp.Embed = isFalse HeyLo.instDecidableEqUnOp.decEq._proof_7
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.Iverson HeyLo.UnOp.Iverson = isTrue HeyLo.instDecidableEqUnOp.decEq._proof_8
• HeyLo.instDecidableEqUnOp.decEq HeyLo.UnOp.NatToENNReal HeyLo.UnOp.NatToENNReal = isTrue HeyLo.instDecidableEqUnOp.decEq._proof_9

@[implicit_reducible]

instance HeyLo.instDecidableEqUnOp {a✝ a✝¹ : Ty} : DecidableEq (UnOp a✝ a✝¹)

Equations

• HeyLo.instDecidableEqUnOp = HeyLo.instDecidableEqUnOp.decEq

inductive HeyLo.QuantOp : Ty → Type

• Inf : QuantOp Ty.ENNReal

  The infimum of a set.

• Sup : QuantOp Ty.ENNReal

  The supremum of a set.

• Forall : QuantOp Ty.Bool

  Boolean forall (equivalent to Inf on the lattice of booleans).

• Exists : QuantOp Ty.Bool

  Boolean exists (equivalent to Sup on the lattice of booleans).

@[implicit_reducible]

instance HeyLo.instToExprQuantOp {a✝ : Ty} : Lean.ToExpr (QuantOp a✝)

Equations

• HeyLo.instToExprQuantOp = { toExpr := HeyLo.instToExprQuantOp.toExpr, toTypeExpr := (Lean.Expr.const `HeyLo.QuantOp []).app (Lean.toExpr a✝) }

def HeyLo.instToExprQuantOp.toExpr {a✝ : Ty} : QuantOp a✝ → Lean.Expr

Equations

• HeyLo.instToExprQuantOp.toExpr HeyLo.QuantOp.Inf = Lean.Expr.const `HeyLo.QuantOp.Inf []
• HeyLo.instToExprQuantOp.toExpr HeyLo.QuantOp.Sup = Lean.Expr.const `HeyLo.QuantOp.Sup []
• HeyLo.instToExprQuantOp.toExpr HeyLo.QuantOp.Forall = Lean.Expr.const `HeyLo.QuantOp.Forall []
• HeyLo.instToExprQuantOp.toExpr HeyLo.QuantOp.Exists = Lean.Expr.const `HeyLo.QuantOp.Exists []

def HeyLo.instDecidableEqQuantOp.decEq {a✝ : Ty} (x✝ x✝¹ : QuantOp a✝) : Decidable (x✝ = x✝¹)

Equations

• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Inf HeyLo.QuantOp.Inf = isTrue HeyLo.instDecidableEqQuantOp.decEq._proof_1
• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Inf HeyLo.QuantOp.Sup = isFalse HeyLo.instDecidableEqQuantOp.decEq._proof_2
• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Sup HeyLo.QuantOp.Inf = isFalse HeyLo.instDecidableEqQuantOp.decEq._proof_3
• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Sup HeyLo.QuantOp.Sup = isTrue HeyLo.instDecidableEqQuantOp.decEq._proof_4
• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Forall HeyLo.QuantOp.Forall = isTrue HeyLo.instDecidableEqQuantOp.decEq._proof_5
• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Forall HeyLo.QuantOp.Exists = isFalse HeyLo.instDecidableEqQuantOp.decEq._proof_6
• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Exists HeyLo.QuantOp.Forall = isFalse HeyLo.instDecidableEqQuantOp.decEq._proof_7
• HeyLo.instDecidableEqQuantOp.decEq HeyLo.QuantOp.Exists HeyLo.QuantOp.Exists = isTrue HeyLo.instDecidableEqQuantOp.decEq._proof_8

@[implicit_reducible]

instance HeyLo.instDecidableEqQuantOp {a✝ : Ty} : DecidableEq (QuantOp a✝)

Equations

• HeyLo.instDecidableEqQuantOp = HeyLo.instDecidableEqQuantOp.decEq

structure HeyLo.Ident : Type

• name : String
• type : Ty

def HeyLo.instToExprIdent.toExpr : Ident → Lean.Expr

Equations

• HeyLo.instToExprIdent.toExpr { name := a, type := a_1 } = ((Lean.Expr.const `HeyLo.Ident.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[implicit_reducible]

instance HeyLo.instToExprIdent : Lean.ToExpr Ident

Equations

• HeyLo.instToExprIdent = { toExpr := HeyLo.instToExprIdent.toExpr, toTypeExpr := Lean.Expr.const `HeyLo.Ident [] }

def HeyLo.instDecidableEqIdent.decEq (x✝ x✝¹ : Ident) : Decidable (x✝ = x✝¹)

Equations

• HeyLo.instDecidableEqIdent.decEq { name := a, type := a_1 } { name := b, type := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance HeyLo.instDecidableEqIdent : DecidableEq Ident

Equations

• HeyLo.instDecidableEqIdent = HeyLo.instDecidableEqIdent.decEq

@[implicit_reducible]

instance HeyLo.instHashableIdent : Hashable Ident

Equations

• HeyLo.instHashableIdent = { hash := HeyLo.instHashableIdent.hash }

def HeyLo.instHashableIdent.hash : Ident → UInt64

Equations

• HeyLo.instHashableIdent.hash { name := a, type := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance HeyLo.instInhabitedIdent : Inhabited Ident

Equations

• HeyLo.instInhabitedIdent = { default := HeyLo.instInhabitedIdent.default }

def HeyLo.instInhabitedIdent.default : Ident

Equations

• HeyLo.instInhabitedIdent.default = { name := default, type := default }

theorem HeyLo.Ident.ext {i j : Ident} (h : i.name = j.name) (h' : i.type = j.type) : i = j

theorem HeyLo.Ident.ext_iff {i j : Ident} : i = j ↔ i.name = j.name ∧ i.type = j.type

def HeyLo.Ident.toLex (i : Ident) : Lex (String × Ty)

Equations

• i.toLex = (i.name, i.type)

@[implicit_reducible]

instance HeyLo.Ident.instLinearOrder : LinearOrder Ident

Equations

• HeyLo.Ident.instLinearOrder = LinearOrder.lift' HeyLo.Ident.toLex HeyLo.Ident.instLinearOrder._proof_2

@[reducible, inline]

abbrev HeyLo.Ty.Γ : Ident → Type

Equations

• HeyLo.Ty.Γ x = x.type.lit

def HeyLo.«term𝔼'[_]» : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev HeyLo.Ty.expr (t : Ty) : Type

Equations

• t.expr = (pGCL.State HeyLo.Ty.Γ → t.lit)

@[implicit_reducible]

instance HeyLo.instToExprRat_heyVL : Lean.ToExpr ℚ

Equations

• HeyLo.instToExprRat_heyVL = { toExpr := fun (r : ℚ) => Lean.mkApp2 (Lean.Expr.const `mkRat []) (Lean.toExpr r.num) (Lean.toExpr r.den), toTypeExpr := Lean.Expr.const `Rat [] }

@[implicit_reducible]

instance HeyLo.instToExprNNRat_heyVL : Lean.ToExpr ℚ≥0

Equations

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

inductive HeyLo.Literal : Ty → Type

• UInt {α : Ty} (h : α.Arith) : ℕ → Literal α

  An unsigned integer literal (123).

• Frac : ℚ≥0 → Literal Ty.ENNReal

  A number literal represented by a fraction.

• Infinity : Literal Ty.ENNReal

  Infinity,

• Bool : _root_.Bool → Literal Ty.Bool

  A boolean literal.

def HeyLo.instDecidableEqLiteral.decEq {a✝ : Ty} (x✝ x✝¹ : Literal a✝) : Decidable (x✝ = x✝¹)

Equations

• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.UInt a_2 a_3) (HeyLo.Literal.UInt b b_1) = if h : a_2 = b then h ▸ if h : a_3 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.UInt h a_1) (HeyLo.Literal.Frac a_2) = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.UInt h a_1) HeyLo.Literal.Infinity = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.UInt h a_1) (HeyLo.Literal.Bool a_2) = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.Frac a_1) (HeyLo.Literal.UInt h a_2) = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.Frac a_1) (HeyLo.Literal.Frac b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.Frac a_1) HeyLo.Literal.Infinity = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq HeyLo.Literal.Infinity (HeyLo.Literal.UInt h a_1) = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq HeyLo.Literal.Infinity (HeyLo.Literal.Frac a_1) = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq HeyLo.Literal.Infinity HeyLo.Literal.Infinity = isTrue HeyLo.instDecidableEqLiteral.decEq._proof_13
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.Bool a_1) (HeyLo.Literal.UInt h a_2) = isFalse ⋯
• HeyLo.instDecidableEqLiteral.decEq (HeyLo.Literal.Bool a_1) (HeyLo.Literal.Bool b) = if h : a_1 = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HeyLo.instDecidableEqLiteral {a✝ : Ty} : DecidableEq (Literal a✝)

Equations

• HeyLo.instDecidableEqLiteral = HeyLo.instDecidableEqLiteral.decEq

def HeyLo.instToExprLiteral.toExpr {a✝ : Ty} : Literal a✝ → Lean.Expr

Equations

• HeyLo.instToExprLiteral.toExpr (HeyLo.Literal.UInt a_2 a_3) = (((Lean.Expr.const `HeyLo.Literal.UInt []).app (Lean.toExpr a✝)).app (Lean.toExpr a_2)).app (Lean.toExpr a_3)
• HeyLo.instToExprLiteral.toExpr (HeyLo.Literal.Frac a_1) = (Lean.Expr.const `HeyLo.Literal.Frac []).app (Lean.toExpr a_1)
• HeyLo.instToExprLiteral.toExpr HeyLo.Literal.Infinity = Lean.Expr.const `HeyLo.Literal.Infinity []
• HeyLo.instToExprLiteral.toExpr (HeyLo.Literal.Bool a_1) = (Lean.Expr.const `HeyLo.Literal.Bool []).app (Lean.toExpr a_1)

@[implicit_reducible]

instance HeyLo.instToExprLiteral {a✝ : Ty} : Lean.ToExpr (Literal a✝)

Equations

• HeyLo.instToExprLiteral = { toExpr := HeyLo.instToExprLiteral.toExpr, toTypeExpr := (Lean.Expr.const `HeyLo.Literal []).app (Lean.toExpr a✝) }

inductive HeyLo.Fun : Ty → Ty → Type

• nfloor : Fun Ty.ENNReal Ty.Nat
• nlog2 : Fun Ty.Nat Ty.Nat

@[implicit_reducible]

instance HeyLo.instDecidableEqFun {a✝ a✝¹ : Ty} : DecidableEq (Fun a✝ a✝¹)

Equations

• HeyLo.instDecidableEqFun = HeyLo.instDecidableEqFun.decEq

def HeyLo.instDecidableEqFun.decEq {a✝ a✝¹ : Ty} (x✝ x✝¹ : Fun a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• HeyLo.instDecidableEqFun.decEq HeyLo.Fun.nfloor HeyLo.Fun.nfloor = isTrue HeyLo.instDecidableEqFun.decEq._proof_1
• HeyLo.instDecidableEqFun.decEq HeyLo.Fun.nlog2 HeyLo.Fun.nlog2 = isTrue HeyLo.instDecidableEqFun.decEq._proof_2

def HeyLo.instToExprFun.toExpr {a✝ a✝¹ : Ty} : Fun a✝ a✝¹ → Lean.Expr

Equations

• HeyLo.instToExprFun.toExpr HeyLo.Fun.nfloor = Lean.Expr.const `HeyLo.Fun.nfloor []
• HeyLo.instToExprFun.toExpr HeyLo.Fun.nlog2 = Lean.Expr.const `HeyLo.Fun.nlog2 []

@[implicit_reducible]

instance HeyLo.instToExprFun {a✝ a✝¹ : Ty} : Lean.ToExpr (Fun a✝ a✝¹)

Equations

• HeyLo.instToExprFun = { toExpr := HeyLo.instToExprFun.toExpr, toTypeExpr := ((Lean.Expr.const `HeyLo.Fun []).app (Lean.toExpr a✝¹)).app (Lean.toExpr a✝) }

inductive HeyLo : HeyLo.Ty → Type

• Call {α β : Ty} : Fun α β → HeyLo α → HeyLo β

  A call to a procedure or function.

• Unary {α β : Ty} : UnOp α β → HeyLo α → HeyLo β
• Binary {α β : Ty} : BinOp α β → HeyLo α → HeyLo α → HeyLo β
• Var : String → (α : Ty) → HeyLo α

  A variable.

• Ite {α : Ty} : HeyLo Ty.Bool → HeyLo α → HeyLo α → HeyLo α

  Boolean if-then-else

• Quant {α : Ty} : QuantOp α → Ident → HeyLo α → HeyLo α

  A quantifier over some variables.

• Subst {α : Ty} (v : Ident) : HeyLo v.type → HeyLo α → HeyLo α

  A substitution.

• Lit {α : Ty} : Literal α → HeyLo α

  A value literal.

def instToExprHeyLo.toExpr {a✝ : HeyLo.Ty} : HeyLo a✝ → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• instToExprHeyLo.toExpr (HeyLo.Call a_3 a_4) = ((((Lean.Expr.const `HeyLo.Call []).app (Lean.toExpr a_2)).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)).app (instToExprHeyLo.toExpr a_4)
• instToExprHeyLo.toExpr (HeyLo.Unary a_3 a_4) = ((((Lean.Expr.const `HeyLo.Unary []).app (Lean.toExpr a_2)).app (Lean.toExpr a✝)).app (Lean.toExpr a_3)).app (instToExprHeyLo.toExpr a_4)
• instToExprHeyLo.toExpr (HeyLo.Var a_2 a✝) = ((Lean.Expr.const `HeyLo.Var []).app (Lean.toExpr a_2)).app (Lean.toExpr a✝)
• instToExprHeyLo.toExpr (HeyLo.Quant a_2 a_3 a_4) = ((((Lean.Expr.const `HeyLo.Quant []).app (Lean.toExpr a✝)).app (Lean.toExpr a_2)).app (Lean.toExpr a_3)).app (instToExprHeyLo.toExpr a_4)
• instToExprHeyLo.toExpr (HeyLo.Lit a_2) = ((Lean.Expr.const `HeyLo.Lit []).app (Lean.toExpr a✝)).app (Lean.toExpr a_2)

@[implicit_reducible]

instance instToExprHeyLo {a✝ : HeyLo.Ty} : Lean.ToExpr (HeyLo a✝)

Equations

• instToExprHeyLo = { toExpr := instToExprHeyLo.toExpr, toTypeExpr := (Lean.Expr.const `HeyLo []).app (Lean.toExpr a✝) }

@[implicit_reducible]

instance instDecidableEqHeyLo {a✝ : HeyLo.Ty} : DecidableEq (HeyLo a✝)

Equations

• instDecidableEqHeyLo = instDecidableEqHeyLo.decEq

def instDecidableEqHeyLo.decEq {a✝ : HeyLo.Ty} (x✝ x✝¹ : HeyLo a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqHeyLo.decEq (HeyLo.Call a_1 a_2) (HeyLo.Unary a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Call a_1 a_2) (HeyLo.Binary a_3 a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Call a_1 a_2) (HeyLo.Var a_3 a✝) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Call a_1 a_2) (a_3.Ite a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Call a_1 a_2) (HeyLo.Quant a_3 a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Call a_1 a_2) (HeyLo.Subst v a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Call a_1 a_2) (HeyLo.Lit a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Unary a_1 a_2) (HeyLo.Call a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Unary a_1 a_2) (HeyLo.Binary a_3 a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Unary a_1 a_2) (HeyLo.Var a_3 a✝) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Unary a_1 a_2) (a_3.Ite a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Unary a_1 a_2) (HeyLo.Quant a_3 a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Unary a_1 a_2) (HeyLo.Subst v a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Unary a_1 a_2) (HeyLo.Lit a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Binary a_1 a_2 a_3) (HeyLo.Call a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Binary a_1 a_2 a_3) (HeyLo.Unary a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Binary a_1 a_2 a_3) (HeyLo.Var a_4 a✝) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Binary a_1 a_2 a_3) (a_4.Ite a_5 a_6) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Binary a_1 a_2 a_3) (HeyLo.Quant a_4 a_5 a_6) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Binary a_1 a_2 a_3) (HeyLo.Subst v a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Binary a_1 a_2 a_3) (HeyLo.Lit a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_1 a✝) (HeyLo.Call a_2 a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_1 a✝) (HeyLo.Unary a_2 a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_1 a✝) (HeyLo.Binary a_2 a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_2 a✝) (HeyLo.Var b a✝) = if h : a_2 = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_1 a✝) (a_2.Ite a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_1 a✝) (HeyLo.Quant a_2 a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_1 a✝) (HeyLo.Subst v a_2 a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Var a_1 a✝) (HeyLo.Lit a_2) = isFalse ⋯
• instDecidableEqHeyLo.decEq (a_1.Ite a_2 a_3) (HeyLo.Call a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (a_1.Ite a_2 a_3) (HeyLo.Unary a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (a_1.Ite a_2 a_3) (HeyLo.Binary a_4 a_5 a_6) = isFalse ⋯
• instDecidableEqHeyLo.decEq (a_1.Ite a_2 a_3) (HeyLo.Var a_4 a✝) = isFalse ⋯
• instDecidableEqHeyLo.decEq (a_1.Ite a_2 a_3) (HeyLo.Quant a_4 a_5 a_6) = isFalse ⋯
• instDecidableEqHeyLo.decEq (a_1.Ite a_2 a_3) (HeyLo.Subst v a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (a_1.Ite a_2 a_3) (HeyLo.Lit a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Quant a_1 a_2 a_3) (HeyLo.Call a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Quant a_1 a_2 a_3) (HeyLo.Unary a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Quant a_1 a_2 a_3) (HeyLo.Binary a_4 a_5 a_6) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Quant a_1 a_2 a_3) (HeyLo.Var a_4 a✝) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Quant a_1 a_2 a_3) (a_4.Ite a_5 a_6) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Quant a_1 a_2 a_3) (HeyLo.Subst v a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Quant a_1 a_2 a_3) (HeyLo.Lit a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Subst v a_1 a_2) (HeyLo.Call a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Subst v a_1 a_2) (HeyLo.Unary a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Subst v a_1 a_2) (HeyLo.Binary a_3 a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Subst v a_1 a_2) (HeyLo.Var a_3 a✝) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Subst v a_1 a_2) (a_3.Ite a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Subst v a_1 a_2) (HeyLo.Quant a_3 a_4 a_5) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Subst v a_1 a_2) (HeyLo.Lit a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_1) (HeyLo.Call a_2 a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_1) (HeyLo.Unary a_2 a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_1) (HeyLo.Binary a_2 a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_1) (HeyLo.Var a_2 a✝) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_1) (a_2.Ite a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_1) (HeyLo.Quant a_2 a_3 a_4) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_1) (HeyLo.Subst v a_2 a_3) = isFalse ⋯
• instDecidableEqHeyLo.decEq (HeyLo.Lit a_2) (HeyLo.Lit b) = if h : a_2 = b then h ▸ isTrue ⋯ else isFalse ⋯

def HeyLo.term𝔼r : Lean.ParserDescr

Equations

• HeyLo.term𝔼r = Lean.ParserDescr.node `HeyLo.term𝔼r 1024 (Lean.ParserDescr.symbol "𝔼r")

def HeyLo.term𝔼b : Lean.ParserDescr

Equations

• HeyLo.term𝔼b = Lean.ParserDescr.node `HeyLo.term𝔼b 1024 (Lean.ParserDescr.symbol "𝔼b")

@[implicit_reducible]

instance instTopHeyLoENNReal : Top (HeyLo HeyLo.Ty.ENNReal)

Equations

• instTopHeyLoENNReal = { top := HeyLo.Lit HeyLo.Literal.Infinity }

@[implicit_reducible]

instance HeyLo.instOfNat {α : Ty} {n : ℕ} (h : α.Arith := by exact default) : OfNat (HeyLo α) n

Equations

• HeyLo.instOfNat h = { ofNat := HeyLo.Lit (HeyLo.Literal.UInt h n) }

@[implicit_reducible]

instance HeyLo.instAdd {α : Ty} (h : α.Arith := by exact default) : Add (HeyLo α)

Equations

• HeyLo.instAdd h = { add := HeyLo.Binary (HeyLo.BinOp.Add h) }

@[implicit_reducible]

instance HeyLo.instSub {α : Ty} (h : α.Arith := by exact default) : Sub (HeyLo α)

Equations

• HeyLo.instSub h = { sub := HeyLo.Binary (HeyLo.BinOp.Sub h) }

@[implicit_reducible]

instance HeyLo.instMul {α : Ty} (h : α.Arith := by exact default) : Mul (HeyLo α)

Equations

• HeyLo.instMul h = { mul := HeyLo.Binary (HeyLo.BinOp.Mul h) }

@[implicit_reducible]

instance HeyLo.instDiv {α : Ty} (h : α.Arith := by exact default) : Div (HeyLo α)

Equations

• HeyLo.instDiv h = { div := HeyLo.Binary (HeyLo.BinOp.Div h) }

@[implicit_reducible]

instance instMinHeyLoENNReal : Min (HeyLo HeyLo.Ty.ENNReal)

Equations

• instMinHeyLoENNReal = { min := HeyLo.Binary HeyLo.BinOp.Inf }

@[implicit_reducible]

instance instMaxHeyLoENNReal : Max (HeyLo HeyLo.Ty.ENNReal)

Equations

• instMaxHeyLoENNReal = { max := HeyLo.Binary HeyLo.BinOp.Sup }

@[implicit_reducible]

instance instHImpHeyLoENNReal : HImp (HeyLo HeyLo.Ty.ENNReal)

Equations

• instHImpHeyLoENNReal = { himp := HeyLo.Binary HeyLo.BinOp.Impl }

@[implicit_reducible]

instance instSDiffHeyLoENNReal : SDiff (HeyLo HeyLo.Ty.ENNReal)

Equations

• instSDiffHeyLoENNReal = { sdiff := fun (a b : HeyLo HeyLo.Ty.ENNReal) => HeyLo.Binary HeyLo.BinOp.CoImpl b a }

@[implicit_reducible]

instance instHNotHeyLo {α : HeyLo.Ty} : HNot (HeyLo α)

Equations

• instHNotHeyLo = { hnot := HeyLo.Unary HeyLo.UnOp.Not }

@[implicit_reducible]

instance instComplHeyLoENNReal : Compl (HeyLo HeyLo.Ty.ENNReal)

Equations

• instComplHeyLoENNReal = { compl := HeyLo.Unary HeyLo.UnOp.Non }

@[implicit_reducible]

instance instIversonHeyLoBoolENNReal : Iverson (HeyLo HeyLo.Ty.Bool) (HeyLo HeyLo.Ty.ENNReal)

Equations

• instIversonHeyLoBoolENNReal = { iver := HeyLo.Unary HeyLo.UnOp.Iverson }

@[reducible]

instance instOfNatHeyLoENNReal {n : ℕ} : OfNat (HeyLo HeyLo.Ty.ENNReal) n

Equations

• instOfNatHeyLoENNReal = HeyLo.instOfNat default

@[reducible]

instance instOfNatHeyLoNat {n : ℕ} : OfNat (HeyLo HeyLo.Ty.Nat) n

Equations

• instOfNatHeyLoNat = HeyLo.instOfNat default

@[reducible]

instance instAddHeyLoENNReal : Add (HeyLo HeyLo.Ty.ENNReal)

Equations

• instAddHeyLoENNReal = HeyLo.instAdd default

@[reducible]

instance instAddHeyLoNat : Add (HeyLo HeyLo.Ty.Nat)

Equations

• instAddHeyLoNat = HeyLo.instAdd default

@[reducible]

instance instSubHeyLoENNReal : Sub (HeyLo HeyLo.Ty.ENNReal)

Equations

• instSubHeyLoENNReal = HeyLo.instSub default

@[reducible]

instance instSubHeyLoNat : Sub (HeyLo HeyLo.Ty.Nat)

Equations

• instSubHeyLoNat = HeyLo.instSub default

@[reducible]

instance instMulHeyLoENNReal : Mul (HeyLo HeyLo.Ty.ENNReal)

Equations

• instMulHeyLoENNReal = HeyLo.instMul default

@[reducible]

instance instMulHeyLoNat : Mul (HeyLo HeyLo.Ty.Nat)

Equations

• instMulHeyLoNat = HeyLo.instMul default

@[reducible]

instance instDivHeyLoENNReal : Div (HeyLo HeyLo.Ty.ENNReal)

Equations

• instDivHeyLoENNReal = HeyLo.instDiv default

@[reducible]

instance instDivHeyLoNat : Div (HeyLo HeyLo.Ty.Nat)

Equations

• instDivHeyLoNat = HeyLo.instDiv default

def HeyLo.subst {α : Ty} (X : HeyLo α) (x : Ident) (Y : HeyLo x.type) : HeyLo α

Equations

• X.subst x Y = HeyLo.Subst x Y X

@[implicit_reducible]

instance instSubstitutionHeyLoIdentType {α : HeyLo.Ty} : Substitution (HeyLo α) fun (v : HeyLo.Ident) => HeyLo v.type

Equations

• instSubstitutionHeyLoIdentType = { subst := fun (X : HeyLo α) (x : (v : HeyLo.Ident) × HeyLo v.type) => X.subst x.fst x.snd }

def HeyLo.Literal.lit {α : Ty} (l : Literal α) : α.lit

Equations

• (HeyLo.Literal.UInt h_2 n).lit = ↑n
• (HeyLo.Literal.UInt h_2 n).lit = n
• (HeyLo.Literal.Frac n).lit = ↑n
• (HeyLo.Literal.Bool b).lit = (b = true)
• HeyLo.Literal.Infinity.lit = ⊤

def HeyLo.Literal.sem {α : Ty} (l : Literal α) : α.expr

Equations

• (HeyLo.Literal.UInt h_2 n).sem = ↑n
• (HeyLo.Literal.UInt h_2 n).sem = ↑n
• (HeyLo.Literal.Frac n).sem = fun (x : pGCL.State HeyLo.Ty.Γ) => ↑n
• (HeyLo.Literal.Bool b).sem = fun (x : pGCL.State HeyLo.Ty.Γ) => b = true
• HeyLo.Literal.Infinity.sem = ⊤

noncomputable def HeyLo.BinOp.sem {α β : Ty} (op : BinOp α β) (l r : α.expr) : β.expr

Equations

• HeyLo.BinOp.CoImpl.sem l_2 r_2 = r_2 \ l_2
• HeyLo.BinOp.Impl.sem l_2 r_2 = l_2 ⇨ r_2
• HeyLo.BinOp.Sup.sem l_2 r_2 = l_2 ⊔ r_2
• HeyLo.BinOp.Inf.sem l_2 r_2 = l_2 ⊓ r_2
• (HeyLo.BinOp.Gt h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => r_3 σ > l_3 σ
• (HeyLo.BinOp.Gt h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => r_3 σ > l_3 σ
• (HeyLo.BinOp.Ge h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ ≥ r_3 σ
• (HeyLo.BinOp.Ge h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ ≥ r_3 σ
• (HeyLo.BinOp.Ne h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ ≠ r_3 σ
• (HeyLo.BinOp.Ne h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ ≠ r_3 σ
• (HeyLo.BinOp.Le h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ ≤ r_3 σ
• (HeyLo.BinOp.Le h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ ≤ r_3 σ
• (HeyLo.BinOp.Lt h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ < r_3 σ
• (HeyLo.BinOp.Lt h_2).sem l_3 r_3 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_3 σ < r_3 σ
• HeyLo.BinOp.Eq.sem l r = fun (σ : pGCL.State HeyLo.Ty.Γ) => l σ = r σ
• HeyLo.BinOp.Or.sem l_2 r_2 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_2 σ ∨ r_2 σ
• HeyLo.BinOp.And.sem l_2 r_2 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_2 σ ∧ r_2 σ
• HeyLo.BinOp.Mod.sem l_2 r_2 = fun (σ : pGCL.State HeyLo.Ty.Γ) => l_2 σ % r_2 σ
• (HeyLo.BinOp.Div h_2).sem l_3 r_3 = l_3 / r_3
• (HeyLo.BinOp.Div h_2).sem l_3 r_3 = l_3 / r_3
• (HeyLo.BinOp.Mul h_2).sem l_3 r_3 = l_3 * r_3
• (HeyLo.BinOp.Mul h_2).sem l_3 r_3 = l_3 * r_3
• (HeyLo.BinOp.Sub h_2).sem l_3 r_3 = l_3 - r_3
• (HeyLo.BinOp.Sub h_2).sem l_3 r_3 = l_3 - r_3
• (HeyLo.BinOp.Add h_2).sem l_3 r_3 = l_3 + r_3
• (HeyLo.BinOp.Add h_2).sem l_3 r_3 = l_3 + r_3

noncomputable def HeyLo.UnOp.sem {α β : Ty} (op : UnOp α β) (x : α.expr) : β.expr

Equations

• HeyLo.UnOp.Not.sem x_3 = ￢x_3
• HeyLo.UnOp.Not.sem x_3 = ￢x_3
• HeyLo.UnOp.Not.sem x_3 = x_3
• HeyLo.UnOp.Non.sem x_2 = ~ x_2
• HeyLo.UnOp.Iverson.sem x_2 = i[x_2]
• HeyLo.UnOp.Embed.sem x_2 = i[x_2] * ⊤
• HeyLo.UnOp.NatToENNReal.sem x_2 = fun (x : pGCL.State HeyLo.Ty.Γ) => ↑(x_2 x)

@[simp]

theorem Bool.iInf_eq {α : Type u_1} (f : α → Bool) : ⨅ (x : α), f x = true ↔ ∀ (x : α), f x = true

@[simp]

theorem Bool.iSup_eq {α : Type u_1} (f : α → Bool) : ⨆ (x : α), f x = true ↔ ∃ (x : α), f x = true

noncomputable def HeyLo.QuantOp.sem {α : Ty} (op : QuantOp α) (x : Ident) (m : α.expr) : α.expr

Equations

• HeyLo.QuantOp.Inf.sem x m_2 = ⨅ (v : x.type.lit), m_2[x ↦ fun (x : pGCL.State HeyLo.Ty.Γ) => v]
• HeyLo.QuantOp.Sup.sem x m_2 = ⨆ (v : x.type.lit), m_2[x ↦ fun (x : pGCL.State HeyLo.Ty.Γ) => v]
• HeyLo.QuantOp.Forall.sem x m_2 = ⨅ (v : x.type.lit), m_2[x ↦ fun (x : pGCL.State HeyLo.Ty.Γ) => v]
• HeyLo.QuantOp.Exists.sem x m_2 = ⨆ (v : x.type.lit), m_2[x ↦ fun (x : pGCL.State HeyLo.Ty.Γ) => v]

@[simp]

theorem HeyLo.QuantOp.Sup_sem_eq_iSup_ennreal {𝒱 : Sort u_1} {e : Ty.ENNReal.expr} [DecidableEq 𝒱] {x : Ident} : Sup.sem x e = ⨆ (v : x.type.lit), e[x ↦ fun (x : pGCL.State Ty.Γ) => v]

@[simp]

theorem HeyLo.QuantOp.Sup_sem_eq_iInf_ennreal {e : Ty.ENNReal.expr} {x : Ident} : Inf.sem x e = ⨅ (v : x.type.lit), e[x ↦ fun (x : pGCL.State Ty.Γ) => v]

noncomputable def HeyLo.Fun.sem {α β : Ty} (f : Fun α β) (m : α.expr) : β.expr

Equations

• HeyLo.Fun.nfloor.sem m_2 = fun (σ : pGCL.State HeyLo.Ty.Γ) => ⌊ENNReal.toReal (m_2 σ)⌋.toNat
• HeyLo.Fun.nlog2.sem m_2 = fun (σ : pGCL.State HeyLo.Ty.Γ) => Nat.log2 (m_2 σ)

noncomputable def HeyLo.sem {α : Ty} (X : HeyLo α) : α.expr

Equations

• (HeyLo.Binary op l r).sem = op.sem l.sem r.sem
• (HeyLo.Lit l).sem = l.sem
• (HeyLo.Subst x v m).sem = m.sem[x ↦ v.sem]
• (HeyLo.Quant op x m).sem = op.sem x m.sem
• (HeyLo.Call f x).sem = f.sem x.sem
• (b.Ite l_2 r_2).sem = fun (σ : pGCL.State HeyLo.Ty.Γ) => if b.sem σ then l_2.sem σ else r_2.sem σ
• (b.Ite l_2 r_2).sem = i[b.sem] * l_2.sem + i[￢b.sem] * r_2.sem
• (b.Ite l_2 r_2).sem = fun (σ : pGCL.State HeyLo.Ty.Γ) => if b.sem σ then l_2.sem σ else r_2.sem σ
• (HeyLo.Var x α).sem = fun (σ : pGCL.State HeyLo.Ty.Γ) => σ { name := x, type := α }
• (HeyLo.Unary op m).sem = op.sem m.sem

theorem QuantOp.Forall_sem_aux {x : HeyLo.Ident} {m : HeyLo.Ty.Bool.expr} {σ : pGCL.State HeyLo.Ty.Γ} : HeyLo.QuantOp.Forall.sem x m σ = ∀ (v : pGCL.State HeyLo.Ty.Γ → HeyLo.Ty.Γ x), (m[x ↦ v]) σ

@[simp]

theorem QuantOp.Forall_sem {x : HeyLo.Ident} {m : HeyLo.Ty.Bool.expr} {σ : pGCL.State HeyLo.Ty.Γ} : HeyLo.QuantOp.Forall.sem x m σ = ∀ (v : x.type.lit), (m[x ↦ fun (x : pGCL.State HeyLo.Ty.Γ) => v]) σ

theorem QuantOp.Exists_sem_aux {x : HeyLo.Ident} {m : HeyLo.Ty.Bool.expr} {σ : pGCL.State HeyLo.Ty.Γ} : HeyLo.QuantOp.Exists.sem x m σ = ∃ (v : pGCL.State HeyLo.Ty.Γ → HeyLo.Ty.Γ x), (m[x ↦ v]) σ

@[simp]

theorem QuantOp.Exists_sem {x : HeyLo.Ident} {m : HeyLo.Ty.Bool.expr} {σ : pGCL.State HeyLo.Ty.Γ} : HeyLo.QuantOp.Exists.sem x m σ = ∃ (v : x.type.lit), (m[x ↦ fun (x : pGCL.State HeyLo.Ty.Γ) => v]) σ

@[simp]

theorem HeyLo.Sup_sem_eq_iSup_ennreal {e : HeyLo Ty.ENNReal} {x : Ident} : (Quant QuantOp.Sup x e).sem = ⨆ (v : x.type.lit), e.sem[x ↦ fun (x : pGCL.State Ty.Γ) => v]

@[simp]

theorem HeyLo.Sup_sem_eq_iInf_ennreal {e : HeyLo Ty.ENNReal} {x : Ident} : (Quant QuantOp.Inf x e).sem = ⨅ (v : x.type.lit), e.sem[x ↦ fun (x : pGCL.State Ty.Γ) => v]

@[simp]

theorem HeyLo.sem_subst {α : Ty} {x : Ident} {v : HeyLo x.type} {X : HeyLo α} : X[x ↦ v].sem = X.sem[x ↦ v.sem]

@[simp]

theorem UnOp.sem_subst {α β : HeyLo.Ty} {subs : List ((a : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → HeyLo.Ty.Γ a))} {op : HeyLo.UnOp α β} {a : α.expr} : (op.sem a)[..subs] = op.sem (a[..subs])

@[simp]

theorem BinOp.sem_subst {α β : HeyLo.Ty} {b : α.expr} {subs : List ((a : HeyLo.Ident) × (pGCL.State HeyLo.Ty.Γ → HeyLo.Ty.Γ a))} {op : HeyLo.BinOp α β} {a : α.expr} : (op.sem a b)[..subs] = op.sem (a[..subs]) (b[..subs])

@[simp]

theorem HeyLo.lit_sem_subst {α : Ty} {subs : List ((a : Ident) × (pGCL.State Ty.Γ → Ty.Γ a))} {l : Literal α} : (Lit l).sem[..subs] = (Lit l).sem

@[simp]

theorem HeyLo.call_sem_subst {α β : Ty} {arg : HeyLo α} {subs : List ((a : Ident) × (pGCL.State Ty.Γ → Ty.Γ a))} {f : Fun α β} : (Call f arg).sem[..subs] = f.sem (arg.sem[..subs])

@[simp]

theorem HeyLo.ite_sem_subst {α : Ty} {c : HeyLo Ty.Bool} {s : List ((a : Ident) × (pGCL.State Ty.Γ → Ty.Γ a))} {a b : HeyLo α} : (c.Ite a b).sem[..s] = fun (σ : pGCL.State Ty.Γ) => if (c.sem[..s]) σ then (a.sem[..s]) σ else (b.sem[..s]) σ

@[simp]

theorem HeyLo.sem_Forall_apply {x : Ident} {σ : pGCL.State Ty.Γ} {c : HeyLo Ty.Bool} : (Quant QuantOp.Forall x c).sem σ ↔ ∀ (v : x.type.lit), c.sem (σ[x ↦ v])

@[simp]

theorem HeyLo.sem_Exists_apply {x : Ident} {σ : pGCL.State Ty.Γ} {c : HeyLo Ty.Bool} : (Quant QuantOp.Exists x c).sem σ ↔ ∃ (v : x.type.lit), c.sem (σ[x ↦ v])

@[reducible, inline]

abbrev HeyLo.Substs : Type

Equations

• HeyLo.Substs = List ((x : HeyLo.Ident) × HeyLo x.type)

def HeyLo.castTy {α β : Ty} (a : HeyLo α) (h : α = β) : HeyLo β

Equations

• a.castTy h = cast ⋯ a

def HeyLo.Substs.find? (subs : Substs) (x : Ident) : Option (HeyLo x.type)

Equations

• subs.find? x = List.findSome? (fun (y : (x : HeyLo.Ident) × HeyLo x.type) => if h : (y.fst == x) = true then some (y.snd.castTy ⋯) else none) subs

def HeyLo.performSubstWith {α : Ty} (a : HeyLo α) (x : Ident) (v : HeyLo x.type) : HeyLo α

Equations

• (HeyLo.Binary op l r).performSubstWith x v = HeyLo.Binary op (l.performSubstWith x v) (r.performSubstWith x v)
• (HeyLo.Lit l).performSubstWith x v = HeyLo.Lit l
• (HeyLo.Subst x_1 v_1 m).performSubstWith x v = HeyLo.Subst x v (HeyLo.Subst x_1 v_1 m)
• (HeyLo.Quant op x_1 m).performSubstWith x v = HeyLo.Subst x v (HeyLo.Quant op x_1 m)
• (HeyLo.Call f x_1).performSubstWith x v = HeyLo.Call f (x_1.performSubstWith x v)
• (b.Ite l r).performSubstWith x v = (b.performSubstWith x v).Ite (l.performSubstWith x v) (r.performSubstWith x v)
• (HeyLo.Var x_1 α).performSubstWith x v = if h : x.name = x_1 ∧ x.type = α then v.castTy ⋯ else HeyLo.Var x_1 α
• (HeyLo.Unary op m).performSubstWith x v = HeyLo.Unary op (m.performSubstWith x v)

theorem HeyLo.performSubstWith_sem {α : Ty} {x : Ident} {v : HeyLo x.type} {m : HeyLo α} : (m.performSubstWith x v).sem = m.sem[x ↦ v.sem]

def HeyLo.performSubst {α : Ty} : HeyLo α → HeyLo α

Equations

• (HeyLo.Binary op l r).performSubst = HeyLo.Binary op l.performSubst r.performSubst
• (HeyLo.Lit l).performSubst = HeyLo.Lit l
• (HeyLo.Subst x v m).performSubst = m.performSubst.performSubstWith x v
• (HeyLo.Quant op x m).performSubst = HeyLo.Quant op x m.performSubst
• (HeyLo.Call f x).performSubst = HeyLo.Call f x.performSubst
• (b.Ite l r).performSubst = b.performSubst.Ite l.performSubst r.performSubst
• (HeyLo.Var x α).performSubst = HeyLo.Var x α
• (HeyLo.Unary op m).performSubst = HeyLo.Unary op m.performSubst

theorem HeyLo.performSubst_sem {α : Ty} {a : HeyLo α} : a.performSubst.sem = a.sem

def HeyLo.opt {α : Ty} : HeyLo α → HeyLo α

Equations

• (HeyLo.Unary HeyLo.UnOp.Not (HeyLo.Lit (HeyLo.Literal.Bool b))).opt = HeyLo.Lit (HeyLo.Literal.Bool (decide ¬b = true))
• (HeyLo.Unary HeyLo.UnOp.Embed (HeyLo.Lit (HeyLo.Literal.Bool true))).opt = HeyLo.Lit (HeyLo.Literal.Frac 1)
• (HeyLo.Unary HeyLo.UnOp.Embed (HeyLo.Lit (HeyLo.Literal.Bool false))).opt = HeyLo.Lit (HeyLo.Literal.Frac 0)
• (HeyLo.Binary op l r).opt = HeyLo.Binary op l.opt r.opt
• (HeyLo.Lit l).opt = HeyLo.Lit l
• (HeyLo.Subst x_1 v m).opt = HeyLo.Subst x_1 v.opt m.opt
• (HeyLo.Quant op x_1 m).opt = HeyLo.Quant op x_1 m.opt
• (HeyLo.Call f x_1).opt = HeyLo.Call f x_1.opt
• (b.Ite l r).opt = b.opt.Ite l.opt r.opt
• (HeyLo.Var x_1 α).opt = HeyLo.Var x_1 α
• (HeyLo.Unary op m).opt = HeyLo.Unary op m.opt

theorem Array.flatMap_sum {α : Type u_1} {β : Type u_2} {A : Array α} {f : α → Array β} [AddMonoid β] : (flatMap f A).sum = (map (fun (a : α) => (f a).sum) A).sum

theorem Array.map_mul_sum {α : Type u_1} {β : Type u_2} [MonoidWithZero β] [AddMonoid β] [LeftDistribClass β] {A : Array α} {s : β} {f : α → β} : (map (fun (x : α) => s * f x) A).sum = s * (map f A).sum

structure HeyLo.Distribution (α : Ty) : Type

• values : Array (HeyLo Ty.ENNReal × HeyLo α)
• prop (σ : pGCL.State Ty.Γ) : (Array.map (fun (x : HeyLo Ty.ENNReal × HeyLo α) => x.1.sem σ) self.values).sum = 1

def HeyLo.instDecidableEqDistribution.decEq {α✝ : Ty} (x✝ x✝¹ : Distribution α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance HeyLo.instDecidableEqDistribution {α✝ : Ty} : DecidableEq (Distribution α✝)

Equations

• HeyLo.instDecidableEqDistribution = HeyLo.instDecidableEqDistribution.decEq

@[implicit_reducible]

instance instToExprDistribution {α : HeyLo.Ty} : Lean.ToExpr (HeyLo.Distribution α)

Equations

• instToExprDistribution = { toExpr := fun (μ : HeyLo.Distribution α) => Lean.toExpr μ.values, toTypeExpr := Lean.Expr.const `HeyLo.Distribution [] }

def HeyLo.Distribution.pure {α : Ty} (v : HeyLo α) : Distribution α

Equations

• HeyLo.Distribution.pure v = { values := #[(1, v)], prop := ⋯ }

def HeyLo.Distribution.bind {α β : Ty} (μ : Distribution α) (f : HeyLo α → Distribution β) : Distribution β

Equations

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

def HeyLo.Distribution.map {α β : Ty} (μ : Distribution α) (f : HeyLo α → HeyLo β) : Distribution β

Equations

• μ.map f = { values := Array.map (fun (x : HeyLo HeyLo.Ty.ENNReal × HeyLo α) => match x with | (p, v) => (p, f v)) μ.values, prop := ⋯ }

@[implicit_reducible]

instance instInhabitedLitType {x : HeyLo.Ident} : Inhabited x.type.lit

Equations

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

@[simp]

theorem HeyLo.Distribution.values_ne_empty {α : Ty} (μ : Distribution α) : μ.values ≠ #[]

@[simp]

theorem HeyLo.Distribution.exists_in_values {α : Ty} (μ : Distribution α) : ∃ (x : HeyLo Ty.ENNReal) (v : HeyLo α), (x, v) ∈ μ.values

@[simp]

theorem Array.sum_replicate {n : ℕ} {α : Type u_1} {x : α} [Semiring α] : (replicate n x).sum = ↑n * x

def HeyLo.Distribution.unif {α : Ty} (vs : Array (HeyLo α)) (h : vs ≠ #[]) : Distribution α

Equations

• HeyLo.Distribution.unif vs h = { values := Array.map (fun (v : HeyLo α) => (HeyLo.Binary (HeyLo.BinOp.Div HeyLo.Yes.yes) 1 (OfNat.ofNat vs.size), v)) vs, prop := ⋯ }

def HeyLo.Distribution.bin {α : Ty} (a : HeyLo α) (p : HeyLo Ty.ENNReal) (b : HeyLo α) : Distribution α

Equations

• HeyLo.Distribution.bin a p b = { values := #[(p ⊓ 1, a), (1 - p ⊓ 1, b)], prop := ⋯ }

def HeyLo.Distribution.flip (p : HeyLo Ty.ENNReal) : Distribution Ty.Bool

Equations

• HeyLo.Distribution.flip p = HeyLo.Distribution.bin (HeyLo.Lit (HeyLo.Literal.Bool true)) p (HeyLo.Lit (HeyLo.Literal.Bool false))

@[simp]

theorem HeyLo.Distribution.pure_map {α a✝ : Ty} {f : HeyLo α → HeyLo a✝} {e : HeyLo α} : (pure e).map f = pure (f e)

@[simp]

theorem HeyLo.Distribution.bin_map {α : Ty} {p : HeyLo Ty.ENNReal} {a✝ : Ty} {f : HeyLo α → HeyLo a✝} {a b : HeyLo α} : (bin a p b).map f = bin (f a) p (f b)

def HeyLo.Distribution.toExpr (μ : Distribution Ty.ENNReal) : HeyLo Ty.ENNReal

Equations

• μ.toExpr = (Array.map (fun (x : HeyLo HeyLo.Ty.ENNReal × HeyLo HeyLo.Ty.ENNReal) => match x with | (p, v) => p * v) μ.values).sum

@[simp]

theorem HeyLo.Distribution.pure_toExpr {a : HeyLo Ty.ENNReal} : (pure a).toExpr = 1 * a + 0

@[simp]

theorem HeyLo.Distribution.bin_toExpr {p a b : HeyLo Ty.ENNReal} : (bin a p b).toExpr = (p ⊓ 1) * a + ((1 - p ⊓ 1) * b + 0)

def HeyLo.not (x : HeyLo Ty.Bool) : HeyLo Ty.Bool

Equations

• x.not = HeyLo.Unary HeyLo.UnOp.Not x

def HeyLo.iver (x : HeyLo Ty.Bool) : HeyLo Ty.ENNReal

Equations

• x.iver = HeyLo.Unary HeyLo.UnOp.Iverson x

def HeyLo.embed (x : HeyLo Ty.Bool) : HeyLo Ty.ENNReal

Equations

• x.embed = HeyLo.Unary HeyLo.UnOp.Embed x

def HeyLo.coembed (x : HeyLo Ty.Bool) : HeyLo Ty.ENNReal

Equations

• x.coembed = HeyLo.Unary HeyLo.UnOp.Embed x.not