From cbeef963a990f2e852a130bf4b8b26beab15d727 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sun, 10 Aug 2025 02:30:55 -0700
Subject: [PATCH] fix: have `unsafe` term produce an opaqueDecl (#9819)

This PR makes the `unsafe t` term create an auxiliary opaque
declaration, rather than an auxiliary definition with opaque
reducibility hints.
---
 src/Lean/Elab/BuiltinNotation.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 3b04ee6af8..73ebbd3a24 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -556,13 +556,12 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     let .const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
     let .defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
     let implName ← mkAuxName `unsafe_impl
-    addDecl <| Declaration.defnDecl {
+    addDecl <| Declaration.opaqueDecl {
       name        := implName
       type        := unsafeDefn.type
       levelParams := unsafeDefn.levelParams
       value       := (← mkOfNonempty unsafeDefn.type)
-      hints       := .opaque
-      safety      := .safe
+      isUnsafe    := false
     }
     setImplementedBy implName unsafeFn
     return mkAppN (Lean.mkConst implName unsafeLvls) t.getAppArgs