From 22bdab67ffe6b3965e398a402547412ae689cd8b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Sep 2020 14:38:26 -0700
Subject: [PATCH] feat: expand `sorry`

---
 src/Lean/Elab/BuiltinNotation.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 249d0b0bb6..4918004c6d 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -284,6 +284,9 @@ fun stx =>
   let arg := stx.getArg 1;
   `(pure $arg)
 
+@[builtinMacro Lean.Parser.Term.«sorry»]  def expandSorry : Macro :=
+fun _ => `(sorryAx _ false)
+
 /-
 TODO
 @[builtinTermElab] def elabsubst : TermElab := expandInfixOp infixR " ▸ " 75