From 46a5f06121af3588f586dec725a8140af70f060b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Aug 2021 16:35:32 -0700
Subject: [PATCH] feat: do not consider dot notation when `isAuxDecl` is true

---
 src/Lean/Elab/Term.lean                | 14 +++++++++++++-
 tests/lean/run/dotNotationRecDecl.lean |  3 +++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/dotNotationRecDecl.lean

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 95d1dcdd91..0485ca2229 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1375,7 +1375,19 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   let view := extractMacroScopes n
   let rec loop (n : Name) (projs : List String) :=
     match lctx.findFromUserName? { view with name := n }.review with
-    | some decl => some (decl.toExpr, projs)
+    | some decl =>
+      if decl.isAuxDecl && !projs.isEmpty then
+        /- We do not consider dot notation for local decls corresponding to recursive functions being defined.
+           The following example would not be elaborated correctly without this case.
+           ```
+            def foo.aux := 1
+            def foo : Nat → Nat
+              | n => foo.aux -- should not be interpreted as `(foo).bar`
+           ```
+         -/
+        none
+      else
+        some (decl.toExpr, projs)
     | none      => match n with
       | Name.str pre s _ => loop pre (s::projs)
       | _                => none
diff --git a/tests/lean/run/dotNotationRecDecl.lean b/tests/lean/run/dotNotationRecDecl.lean
new file mode 100644
index 0000000000..b8be932724
--- /dev/null
+++ b/tests/lean/run/dotNotationRecDecl.lean
@@ -0,0 +1,3 @@
+def foo.aux := 1
+def foo : Nat → Nat
+  | n => foo.aux