We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 02bcc41 commit 79e0306Copy full SHA for 79e0306
src/Lean/Compiler/LCNF/JoinPoints.lean
@@ -45,7 +45,7 @@ structure FindCtx where
45
A map from function declarations that are currently in scope to their
46
definition depth.
47
-/
48
- scope : PersistentHashMap FVarId Nat := {}
+ scope : FVarIdMap Nat := {}
49
/--
50
The current function binder we are inside of if any.
51
@@ -187,7 +187,7 @@ where
187
eraseCandidate fvarId
188
else
189
let currDepth := (← read).definitionDepth
190
- let calleeDepth := (← read).scope.find! fvarId
+ let calleeDepth := (← read).scope.get! fvarId
191
if currDepth == calleeDepth then
192
/-
193
we are in a situation like:
0 commit comments