From 12acbaf392a8926895e3eafd4c0df2fa87504b33 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 20 Sep 2020 07:50:29 -0700
Subject: [PATCH] doc: `resolveGlobalName`

---
 src/Lean/Elab/Term.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 316c81aeaf..f8e7665832 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1169,6 +1169,13 @@ candidates.foldlM
     pure $ (const, projs) :: result)
   []
 
+/-
+  Given a name `n`, return a list of possible interpretations.
+  Each interpretation is a pair `(declName, fieldList)`, where `declName`
+  is the name of a declaration in the current environment, and `fieldList` are
+  (potential) field names.
+  The pair is needed because in Lean `.` may be part of a qualified name or
+  a field (aka dot-notation). -/
 def resolveGlobalName (n : Name) : TermElabM (List (Name × List String)) := do
 env ← getEnv;
 currNamespace ← getCurrNamespace;