rfc: sorry should show decl name

Stream: lean4

[Alok Singh]

def a : Nat := sorry
-- declaration uses 'sorry'

could this error message say something like declaration 'a' uses 'sorry'. the sorry is goto-def able, but just naming the declaration is handy too.

[Kenny Lau]

is this coming from looking at "all messages"? I don't quite understand this suggestion because the warning message is exactly coming from where the declaration is.

[Kenny Lau]

it's just like if you make an error like:

def a : Nat := 3 ++ 3
/-
failed to synthesize
  HAppend Nat Nat Nat
-/

the error messasge and the red underline tell you what is wrong

[Alok Singh]

My markdown formatting was off, it should be declaration $DECL_NAME uses 'sorry' on top of the line/col info.

[Kenny Lau]

I understand what you mean by a, I meant that I don't understand why this is necessary.

[Eric Wieser]

(deleted)

[Kyle Miller]

Sure, seems reasonable. I thought about adding this while making sorry go-to-def-able, but didn't to keep the PR's diff small. If anyone implements this, please use backticks instead of ', both for the constant and the sorry.