From cb5a6a5a2f5c0efeec638e9f7f80362e50ecf502 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 11 Aug 2019 16:08:31 -0700
Subject: [PATCH] feat(library/init/lean/elaborator/resolvename): add
 `preresolveNames` for setting `Syntax.ident` presolved field

---
 library/init/lean/elaborator/resolvename.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/library/init/lean/elaborator/resolvename.lean b/library/init/lean/elaborator/resolvename.lean
index 4a388ae05f..1bd9fdb7e0 100644
--- a/library/init/lean/elaborator/resolvename.lean
+++ b/library/init/lean/elaborator/resolvename.lean
@@ -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