From 70f615d074f5382ffbebf3ce03846a8ac5d2e7e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Sep 2022 15:39:58 -0700 Subject: [PATCH] fix: avoid "unknown constant" error message for auxiliary declarations --- src/Lean/Compiler/LCNF/Simp.lean | 2 +- src/Lean/Compiler/LCNF/Stage1.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index 0a9b01814c..6adf31691e 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -855,7 +855,7 @@ simplification opportunities by eta-expanding them. def etaPolyApp? (letDecl : LetDecl) : OptionT SimpM FunDecl := do guard <| (← read).config.etaPoly let .const declName _ := letDecl.value.getAppFn | failure - let info ← getConstInfo declName + let some info := (← getEnv).find? declName | failure guard <| hasLocalInst info.type guard <| !(← Meta.isInstance declName) let some decl ← getStage1Decl? declName | failure diff --git a/src/Lean/Compiler/LCNF/Stage1.lean b/src/Lean/Compiler/LCNF/Stage1.lean index d93d49a67f..de1ed126d4 100644 --- a/src/Lean/Compiler/LCNF/Stage1.lean +++ b/src/Lean/Compiler/LCNF/Stage1.lean @@ -37,7 +37,7 @@ def getStage1Decl? (declName : Name) : CoreM (Option Decl) := do match stage1Ext.getState (← getEnv) |>.decls.find? declName with | some decl => return decl | none => - let info ← getConstInfo declName + let some info := (← getEnv).find? declName | return none if info.hasValue then let decls ← compileStage1 info.all.toArray return decls.find? fun decl => declName == decl.name