def HeyLo.Syntax.cheylo_var.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cheylo_var : Category

Equations

• Lean.Parser.Category.cheylo_var = { }

def HeyLo.Syntax.«termHeylo_var_{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cheylo_vars.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cheylo_vars : Category

Equations

• Lean.Parser.Category.cheylo_vars = { }

def HeyLo.Syntax.«termHeylo_vars_{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cheylo_dist.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cheylo_dist : Category

Equations

• Lean.Parser.Category.cheylo_dist = { }

def HeyLo.Syntax.«termHeylo_dist_{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cheylo.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cheylo : Category

Equations

• Lean.Parser.Category.cheylo = { }

def HeyLo.Syntax.«termHeylo_{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cheyvl.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cheyvl : Category

Equations

• Lean.Parser.Category.cheyvl = { }

def HeyLo.Syntax.«termHeyvl_{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cspGCL.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cspGCL : Category

Equations

• Lean.Parser.Category.cspGCL = { }

def HeyLo.Syntax.«termSpgcl_{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo_var@_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheylo_var@_» = Lean.ParserDescr.node `HeyLo.Syntax.«cheylo_var@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def HeyLo.Syntax.«cheylo_vars@_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheylo_vars@_» = Lean.ParserDescr.node `HeyLo.Syntax.«cheylo_vars@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def HeyLo.Syntax.«cheylo_dist@_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheylo_dist@_» = Lean.ParserDescr.node `HeyLo.Syntax.«cheylo_dist@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def HeyLo.Syntax.«cheylo@_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheylo@_» = Lean.ParserDescr.node `HeyLo.Syntax.«cheylo@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def HeyLo.Syntax.«cheyvl@_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheyvl@_» = Lean.ParserDescr.node `HeyLo.Syntax.«cheyvl@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def HeyLo.Syntax.«cspGCL@_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cspGCL@_» = Lean.ParserDescr.node `HeyLo.Syntax.«cspGCL@_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "@") (Lean.ParserDescr.cat `term 1024))

def HeyLo.Syntax.cheylo_var_ : Lean.ParserDescr

Equations

• HeyLo.Syntax.cheylo_var_ = Lean.ParserDescr.node `HeyLo.Syntax.cheylo_var_ 1022 (Lean.ParserDescr.const `ident)

def HeyLo.Syntax.cheylo_ : Lean.ParserDescr

Equations

• HeyLo.Syntax.cheylo_ = Lean.ParserDescr.node `HeyLo.Syntax.cheylo_ 1022 (Lean.ParserDescr.const `num)

def HeyLo.Syntax.«cheylo⊤» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheylo⊤» = Lean.ParserDescr.node `HeyLo.Syntax.«cheylo⊤» 1024 (Lean.ParserDescr.symbol "⊤")

def HeyLo.Syntax.cheylo__ : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo[_]» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo_*_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_*_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_*_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " * ") (Lean.ParserDescr.cat `cheylo 71))

def HeyLo.Syntax.«cheylo_/_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_/_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_/_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " / ") (Lean.ParserDescr.cat `cheylo 71))

def HeyLo.Syntax.«cheylo_+_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_+_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_+_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `cheylo 66))

def HeyLo.Syntax.«cheylo_-_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_-_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_-_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `cheylo 66))

def HeyLo.Syntax.«cheylo¬_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheylo¬_» = Lean.ParserDescr.node `HeyLo.Syntax.«cheylo¬_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `cheylo 40))

def HeyLo.Syntax.«cheylo↑_» : Lean.ParserDescr

Equations

• HeyLo.Syntax.«cheylo↑_» = Lean.ParserDescr.node `HeyLo.Syntax.«cheylo↑_» 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↑") (Lean.ParserDescr.cat `cheylo 80))

def HeyLo.Syntax.«cheylo_<_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_<_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_<_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " < ") (Lean.ParserDescr.cat `cheylo 51))

def HeyLo.Syntax.«cheylo_≤_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_≤_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_≤_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ ") (Lean.ParserDescr.cat `cheylo 51))

def HeyLo.Syntax.«cheylo_<=_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_<=_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_<=_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <= ") (Lean.ParserDescr.cat `cheylo 51))

def HeyLo.Syntax.«cheylo_>=_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_>=_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_>=_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >= ") (Lean.ParserDescr.cat `cheylo 51))

def HeyLo.Syntax.«cheylo_≥_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_≥_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_≥_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ ") (Lean.ParserDescr.cat `cheylo 51))

def HeyLo.Syntax.«cheylo_>_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_>_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_>_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " > ") (Lean.ParserDescr.cat `cheylo 51))

def HeyLo.Syntax.«cheylo_=_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_=_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_=_» 45 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " = ") (Lean.ParserDescr.cat `cheylo 46))

def HeyLo.Syntax.«cheylo_!=_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_!=_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_!=_» 45 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " != ") (Lean.ParserDescr.cat `cheylo 46))

def HeyLo.Syntax.«cheylo_≠_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_≠_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_≠_» 45 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠ ") (Lean.ParserDescr.cat `cheylo 46))

def HeyLo.Syntax.«cheylo_∧_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_∧_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_∧_» 35 35 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `cheylo 36))

def HeyLo.Syntax.«cheylo_∨_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_∨_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_∨_» 35 35 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `cheylo 36))

def HeyLo.Syntax.«cheylo_→_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheylo_→_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheylo_→_» 35 35 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " → ") (Lean.ParserDescr.cat `cheylo 36))

def HeyLo.Syntax.«cheylo⨅_,_» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo⨆_,_» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo∀_,_» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo∃_,_» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo(_)_1» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo_distFlip(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheylo_distBin(_,_,_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cspGCL_ : Lean.ParserDescr

Equations

• HeyLo.Syntax.cspGCL_ = Lean.ParserDescr.node `HeyLo.Syntax.cspGCL_ 1022 (Lean.ParserDescr.const `ident)

def HeyLo.Syntax.«cspGCL_:=_» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cspGCL_;_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cspGCL_;_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cspGCL_;_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ; ") (Lean.ParserDescr.cat `cspGCL 0))

def HeyLo.Syntax.«cspGCL{_}[_]{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cspGCL{_}[]{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cspGCLWhile__Inv(_){_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cspGCLTick(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cspGCLObserve(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cspGCLIf_Then_Else_End : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.cheyvl_ : Lean.ParserDescr

Equations

• HeyLo.Syntax.cheyvl_ = Lean.ParserDescr.node `HeyLo.Syntax.cheyvl_ 1022 (Lean.ParserDescr.const `ident)

def HeyLo.Syntax.«cheyvl_:≈_» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlReward(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvl_;_» : Lean.TrailingParserDescr

Equations

• HeyLo.Syntax.«cheyvl_;_» = Lean.ParserDescr.trailingNode `HeyLo.Syntax.«cheyvl_;_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ; ") (Lean.ParserDescr.cat `cheyvl 0))

def HeyLo.Syntax.«cheyvlIf_(⊓)_{_}Else{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlAssert(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlAssume(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlHavoc(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlHavocs(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlIf_(⊔)_{_}Else{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlCoassert(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlCoassume(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlCohavoc(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlCohavocs(_)» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlIf_(_)_{_}Else{_}» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.«cheyvlIf_(_)_{_}» : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev HeyLo.Syntax.x : Ident

Equations

• HeyLo.Syntax.x = { name := "x", type := HeyLo.Ty.ENNReal }

@[reducible, inline]

abbrev HeyLo.Syntax.y : Ident

Equations

• HeyLo.Syntax.y = { name := "y", type := HeyLo.Ty.ENNReal }

@[reducible, inline]

abbrev HeyLo.Syntax.b : Ident

Equations

• HeyLo.Syntax.b = { name := "b", type := HeyLo.Ty.Bool }

@[reducible, inline]

abbrev HeyLo.Syntax.z : Ident

Equations

• HeyLo.Syntax.z = { name := "z", type := HeyLo.Ty.Nat }

@[reducible, inline]

abbrev HeyLo.Syntax.n : Ident

Equations

• HeyLo.Syntax.n = { name := "n", type := HeyLo.Ty.Nat }

def HeyLo.Syntax.VarUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

partial def HeyLo.Syntax.unexpandAexp : Lean.TSyntax `term → Lean.PrettyPrinter.UnexpandM (Lean.TSyntax `cheylo)

def HeyLo.Syntax.BinaryUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.LitUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.«term⟦_⟧'» : Lean.ParserDescr

Equations

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

def HeyLo.Syntax.semUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.skipUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.assignUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.seqUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.probUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.nonDetUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.loopUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.tickUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.observeUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.iteUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.HeyVL.skipUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.ifUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.rewardUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.Distribution.flipUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.Distribution.binUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.heyvlAssignUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.heyvlSeqUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.ifInfUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.assertUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.assumeUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.havocUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.validateUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.ifSupUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.coassertUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.coassumeUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.cohavocUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

def HeyLo.Syntax.covalidateUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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