Defines the assert_no_sorry command.

Throws an error if the given identifier uses sorryAx.

def commandAssert_no_sorry_ : Lean.ParserDescr

Throws an error if the given identifier uses sorryAx.

Equations

• commandAssert_no_sorry_ = Lean.ParserDescr.node `commandAssert_no_sorry_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "assert_no_sorry ") (Lean.ParserDescr.const `ident))