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

feat(library/init/lean/elaborator/resolvename): add preresolveNames for setting Syntax.ident presolved field

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-11 16:08:31 -07:00
parent cea1fa3036
commit cb5a6a5a2f
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/init/lean/elaborator/resolvename.lean
View file

@ -66,5 +66,16 @@ do env ← getEnv;
openDecls ← getOpenDecls;
pure $ resolveNameAux env ns openDecls id 0
private partial def preresolveNamesAux {α} (env : Environment) (ns : Name) (openDecls : List OpenDecl) : Syntax α → Syntax α
| Syntax.node k args => Syntax.node k (args.map preresolveNamesAux)
| Syntax.ident info rawVal val _ => Syntax.ident info rawVal val (resolveNameAux env ns openDecls val 0)
| stx => stx
def preresolveNames {α} (stx : Syntax α) : Elab (Syntax α) :=
do env ← getEnv;
ns ← getNamespace;
openDecls ← getOpenDecls;
pure $ preresolveNamesAux env ns openDecls stx
end Elab
end Lean