sorry in def doesn't warn

Stream: new members

[Alok Singh]

this gives no warnings about the use of sorry. if i don't have sorry in the type signature, then the sorry in the body is at least warned about

theorem sorryInStmt {n: Nat} (f: Fin n → α) (i: Fin n)
  : (ofFn f)[i]'sorry = f i
  := sorry

[Sebastian Ullrich]

Only because it fails before it even gets to the sorry. Could you please provide an #mwe?

[Robin Arnez]

If you mean

theorem sorryInStmt {n : Nat} (f : Fin n → α) (i : Fin n) : (List.ofFn f)[i]'sorry = f i := sorry

then it does warn for me.