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

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