Skip to content

Commit 9982bab

Browse files
authored
perf: Environment.find? should not block on privacy mismatch (#8472)
This PR avoids name resolution blocking on the elaboration of a theorem's proof when looking up the theorem name.
1 parent be51365 commit 9982bab

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/Lean/Environment.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -454,6 +454,9 @@ private partial def AsyncConsts.findRec? (aconsts : AsyncConsts) (declName : Nam
454454
let c ← aconsts.findPrefix? declName
455455
if c.constInfo.name == declName then
456456
return c
457+
-- If privacy is the only difference between `declName` and `findPrefix?` result, we can assume
458+
-- `declName` does not exist according to the `add` invariant
459+
guard <| privateToUserName c.constInfo.name != privateToUserName declName
457460
let aconsts ← c.consts.get.get? AsyncConsts
458461
AsyncConsts.findRec? aconsts declName
459462

0 commit comments

Comments
 (0)