Skip to content

Commit 5af9444

Browse files
committed
fix: finding IR of in-lean compiled decls
1 parent 7f34a3f commit 5af9444

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/Lean/Compiler/IR/CompilerM.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,8 @@ def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
162162
-- it can also see the LCNF)
163163
findAtSorted? (declMapExt.getModuleIREntries env modIdx) declName <|>
164164
-- (closure of) `meta def`; will report `.extern`s for other `def`s so needs to come second
165-
findAtSorted? (declMapExt.getModuleEntries env modIdx) declName
165+
findAtSorted? (declMapExt.getModuleEntries env modIdx) declName <|>
166+
(declMapExt.getState env |>.find? declName)
166167
| none => declMapExt.getState env |>.find? declName
167168

168169
def findDecl (n : Name) : CompilerM (Option Decl) :=

0 commit comments

Comments
 (0)