Defines the assert_no_sorry
command. #
Throws an error if the given identifier uses sorryAx.
Throws an error if the given identifier uses sorryAx.
Mathlib.Util.AssertNoSorry
assert_no_sorry
command. #Throws an error if the given identifier uses sorryAx.
Throws an error if the given identifier uses sorryAx.