Graded Do-Notation

Provides gdo blocks that desugar into gbind/gpure calls, mirroring Lean's built-in do notation for graded monads. An optional trailing grade_by element supplies a proof that the computed grade equals the expected one.

def doElemGrade_by_ : Lean.ParserDescr

Equations

• doElemGrade_by_ = Lean.ParserDescr.node `doElemGrade_by_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "grade_by ") (Lean.ParserDescr.cat `term 0))

def gdoNotation : Lean.ParserDescr

Equations

• gdoNotation = Lean.ParserDescr.node `gdoNotation 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "gdo ") (Lean.ParserDescr.const `doSeq))

def expandGDo : Lean.Macro

Equations

• expandGDo stx = do let a ← expandGDoBlock✝ stx[1] pure a.raw