def sorryWithMsg : Lean.ParserDescr

Equations

• sorryWithMsg = Lean.ParserDescr.node `sorryWithMsg 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "sorryM" false) (Lean.ParserDescr.const `str))

def evalSorryWithMsg : Lean.Elab.Tactic.Tactic

Equations

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