feat: delaborate sorryAx

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -590,4 +590,10 @@ def delabDo : Delab := whenPPOption getPPNotation do
   let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem))
   `(do $items:doSeqItem*)
 
+@[builtinDelab app.sorryAx]
+def delabSorryAx : Delab := whenPPOption getPPNotation do
+  unless (← getExpr).isAppOfArity ``sorryAx 2 do
+    failure
+  `(sorry)
+
 end Lean.PrettyPrinter.Delaborator

tests/lean/255.lean.expected.out

@@ -1,6 +1,6 @@
 id x : α
 id x✝ : α
 255.lean:16:7-16:8: error: unknown constant 'x✝'
-id (sorryAx ?m) : ?m
+id sorry : ?m
 255.lean:20:9-20:10: error: unknown constant 'x✝'
-id (sorryAx ?m) : ?m
+id sorry : ?m

tests/lean/StxQuot.lean.expected.out

@@ -40,5 +40,5 @@ StxQuot.lean:77:33: error: expected parser to return exactly one syntax object
 "#[(numLit \"1\"), [(numLit \"2\") (numLit \"3\")], (numLit \"4\")]"
 "#[(numLit \"2\")]"
 StxQuot.lean:90:39-90:44: error: unexpected antiquotation splice
-fun (a : ?m) => sorryAx (?m a) : (a : ?m) → ?m a
+fun (a : ?m) => sorry : (a : ?m) → ?m a
 "#[(some 1), (some 2)]"

tests/lean/namedHoles.lean.expected.out

@@ -11,7 +11,7 @@ g ?m ?m : Nat
 foo (fun (x : Nat) => ?m x) ?m : Nat
 bla ?m fun (x : Nat) => ?m : Nat
 namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
-boo (fun (x : Nat) => ?m x) fun (y : Bool) => sorryAx Nat : Nat
+boo (fun (x : Nat) => ?m x) fun (y : Bool) => sorry : Nat
 11
 12
 namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context