diff --git a/src/Lean/Compiler/LCNF/PhaseExt.lean b/src/Lean/Compiler/LCNF/PhaseExt.lean index 8497046ac0..6b532c8036 100644 --- a/src/Lean/Compiler/LCNF/PhaseExt.lean +++ b/src/Lean/Compiler/LCNF/PhaseExt.lean @@ -59,6 +59,12 @@ def Decl.saveBase (decl : Decl) : CoreM Unit := def Decl.saveMono (decl : Decl) : CoreM Unit := modifyEnv (saveMonoDeclCore · decl) +def Decl.save (decl : Decl) : CompilerM Unit := do + match (← getPhase) with + | .base => decl.saveBase + | .mono => decl.saveMono + | _ => unreachable! + def getDeclAt? (declName : Name) (phase : Phase) : CoreM (Option Decl) := match phase with | .base => getBaseDecl? declName