Documentation

Mathlib.Util.AssertNoSorry

Defines the assert_no_sorry command. #

Throws an error if the given identifier uses sorryAx.

source
def commandAssert_no_sorry_ :
Lean.ParserDescr

Throws an error if the given identifier uses sorryAx.

Instances For