max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Decl.save

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-08 18:33:26 -07:00
parent 48d3bbdde9
commit 3c90b2fd3e
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Compiler/LCNF/PhaseExt.lean
View file

@ -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