Graded Do-Notation

Provides a gdo block that desugars 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 GradedDo.gdoElab : Lean.ParserDescr

Equations

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

def GradedDo.elabGDo : Lean.Elab.Term.TermElab

Equations

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

def GradedDo.gradeBy : Lean.ParserDescr

Equations

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