From a8d6178e19a4b773bba4ecd6aff8a49b01db7491 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 30 May 2023 17:09:50 -0400
Subject: [PATCH] feat: implement `have this` (part 2)

---
 src/Lean/Elab/Deriving/DecEq.lean    |  2 +-
 src/Lean/Elab/Do.lean                | 14 +++++++-------
 tests/lean/1021.lean.expected.out    |  8 ++++----
 tests/lean/StxQuot.lean.expected.out |  2 +-
 4 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 8a7c66136b..9e655ccddf 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -166,7 +166,7 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
       fun x y =>
         if h : x.toCtorIdx = y.toCtorIdx then
           -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.
-          isTrue (by first | refine_lift let_fun aux := congrArg $ofNatIdent h; ?_; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
+          isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
         else
           isFalse fun h => by subst h; contradiction
   )
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index e8cb54516e..847791bc12 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -624,11 +624,11 @@ def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
   -- leading_parser "let " >> optional "mut " >> letDecl
   getLetDeclVars doLet[2]
 
-def getHaveIdLhsVar (optIdent : Syntax) : TermElabM Var :=
-  if optIdent.isNone then
-    `(this)
+def getHaveIdLhsVar (optIdent : Syntax) : Var :=
+  if optIdent.getKind == hygieneInfoKind then
+    HygieneInfo.mkIdent optIdent[0] `this
   else
-    pure optIdent[0]
+    optIdent
 
 def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := do
   -- doHave := leading_parser "have " >> Term.haveDecl
@@ -636,13 +636,13 @@ def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := do
   let arg := doHave[1][0]
   if arg.getKind == ``Parser.Term.haveIdDecl then
     -- haveIdDecl := leading_parser atomic (haveIdLhs >> " := ") >> termParser
-    -- haveIdLhs := optional (ident >> many (ppSpace >> letIdBinder)) >> optType
-    return #[← getHaveIdLhsVar arg[0]]
+    -- haveIdLhs := (binderIdent <|> hygieneInfo) >> many letIdBinder >> optType
+    return #[getHaveIdLhsVar arg[0]]
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
   else if arg.getKind == ``Parser.Term.haveEqnsDecl then
     -- haveEqnsDecl := leading_parser haveIdLhs >> matchAlts
-    return #[← getHaveIdLhsVar arg[0]]
+    return #[getHaveIdLhsVar arg[0]]
   else
     throwError "unexpected kind of have declaration"
 
diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out
index c986018f74..59be053f7b 100644
--- a/tests/lean/1021.lean.expected.out
+++ b/tests/lean/1021.lean.expected.out
@@ -1,8 +1,8 @@
-some { range := { pos := { line := 167, column := 42 },
+some { range := { pos := { line := 175, column := 42 },
              charUtf16 := 42,
-             endPos := { line := 173, column := 31 },
+             endPos := { line := 181, column := 31 },
              endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 167, column := 46 },
+  selectionRange := { pos := { line := 175, column := 46 },
                       charUtf16 := 46,
-                      endPos := { line := 167, column := 58 },
+                      endPos := { line := 175, column := 58 },
                       endCharUtf16 := 58 } }
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index b1203c8845..685d3a2f88 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -40,7 +40,7 @@ StxQuot.lean:19:15: error: expected term
 "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n    \"=>\"\n    («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))"
 "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]"
 "1"
-"(Term.sufficesDecl [] `x._@.UnhygienicMain._hyg.1 (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))"
+"(Term.sufficesDecl\n (hygieneInfo `_@.UnhygienicMain._hyg.1)\n `x._@.UnhygienicMain._hyg.1\n (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))"
 "#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]"
 "#[(num \"2\")]"
 StxQuot.lean:95:39-95:44: error: unexpected antiquotation splice