From 1945ebd27569f78e79d280a720725f084e95f5f7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 25 Jan 2021 17:19:08 +0100
Subject: [PATCH] feat: delaborate `sorryAx`

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 6 ++++++
 tests/lean/255.lean.expected.out                 | 4 ++--
 tests/lean/StxQuot.lean.expected.out             | 2 +-
 tests/lean/namedHoles.lean.expected.out          | 2 +-
 4 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index b81d9e30e5..d2da63054b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/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
diff --git a/tests/lean/255.lean.expected.out b/tests/lean/255.lean.expected.out
index 1bb006b489..a854e5268a 100644
--- a/tests/lean/255.lean.expected.out
+++ b/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
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 5fe29a5d03..a9cd9b6a42 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/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)]"
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index ba502a68fb..501d13c329 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/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