From a17832ba1492fe1135dfd5952238e3f41fc043e7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 8 Feb 2024 17:24:02 -0800
Subject: [PATCH] chore: add `unsafe` term builtin parser

---
 src/Init/Notation.lean        | 13 -------------
 src/Lean/Parser/Term.lean     | 15 ++++++++++++++-
 src/Lean/Util/TermUnsafe.lean |  2 ++
 3 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 259e388f45..87d783870f 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -462,19 +462,6 @@ expected type is known. So, `without_expected_type` is not effective in this cas
 -/
 macro "without_expected_type " x:term : term => `(let aux := $x; aux)
 
-/--
-`unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
-body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
-wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
-but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
-the compiler is unable to guarantee the safety of the operation.
-
-For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
-you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
-particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
--/
-syntax (name := Lean.Parser.Term.unsafe) "unsafe " term : term
-
 namespace Lean
 
 /--
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index efdceb489b..b4de1bbd3a 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich
+Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
 -/
 import Lean.Parser.Attr
 import Lean.Parser.Level
@@ -601,6 +601,19 @@ def matchAltsWhereDecls := leading_parser
 @[builtin_term_parser] def noindex := leading_parser
   "no_index " >> termParser maxPrec
 
+/--
+`unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
+body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
+wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
+but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
+the compiler is unable to guarantee the safety of the operation.
+
+For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
+you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
+particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
+-/
+@[builtin_term_parser] def «unsafe» := leading_parser:leadPrec "unsafe " >> termParser
+
 /-- `binrel% r a b` elaborates `r a b` as a binary relation using the type propogation protocol in `Lean.Elab.Extra`. -/
 @[builtin_term_parser] def binrel := leading_parser
   "binrel% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec
diff --git a/src/Lean/Util/TermUnsafe.lean b/src/Lean/Util/TermUnsafe.lean
index 535845cf64..7f1bae6649 100644
--- a/src/Lean/Util/TermUnsafe.lean
+++ b/src/Lean/Util/TermUnsafe.lean
@@ -7,6 +7,8 @@ import Lean.Elab.ElabRules
 import Lean.Meta.Closure
 import Lean.Compiler.ImplementedByAttr
 
+#exit
+
 /-!
 Defines term syntax to call unsafe functions.