max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: have unsafe term produce an opaqueDecl (#9819)

Browse source 
This PR makes the `unsafe t` term create an auxiliary opaque
declaration, rather than an auxiliary definition with opaque
reducibility hints.
This commit is contained in:
Kyle Miller 2025-08-10 02:30:55 -07:00 • committed by GitHub
parent 544f9912b7
commit cbeef963a9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/BuiltinNotation.lean
View file

@ -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