feat: implement have this (part 2)

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
   )

src/Lean/Elab/Do.lean

@@ -624,25 +624,25 @@ 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
   -- haveDecl := leading_parser haveIdDecl <|> letPatDecl <|> haveEqnsDecl
   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"
 

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 } }

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