feat: multiple delta, delta conv, unfold

src/Init/Conv.lean

@@ -82,13 +82,13 @@ syntax (name := change) "change " term : conv
 Like the `delta` tactic, this ignores any definitional equations and uses
 primitive delta-reduction instead, which may result in leaking implementation details.
 Users should prefer `unfold` for unfolding definitions. -/
-syntax (name := delta) "delta " ident : conv
+syntax (name := delta) "delta " ident,+ : conv
 
 /-- `unfold foo` unfolds all occurrences of `foo` in the target.
 Like the `unfold` tactic, this uses equational lemmas for the chosen definition
 to rewrite the target. For recursive definitions,
 only one layer of unfolding is performed. -/
-syntax (name := unfold) "unfold " ident : conv
+syntax (name := unfold) "unfold " ident,+ : conv
 
 /-- `pattern pat` traverses to the first subterm of the target that matches `pat`. -/
 syntax (name := pattern) "pattern " term : conv

src/Lean/Elab/Tactic/Conv/Delta.lean

@@ -10,8 +10,8 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 @[builtinTactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
-  let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) (· == declName)
+  let declNames ← stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
+  let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) declNames.contains
   changeLhs lhsNew
 
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Conv/Unfold.lean

@@ -10,7 +10,8 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 @[builtinTactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
-  applySimpResult (← unfold (← getLhs) declName)
+  for declNameId in stx[1].getArgs do
+    let declName ← resolveGlobalConstNoOverloadWithInfo declNameId
+    applySimpResult (← unfold (← getLhs) declName)
 
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Delta.lean

@@ -10,28 +10,30 @@ import Lean.Elab.Tactic.Location
 namespace Lean.Elab.Tactic
 open Meta
 
-def deltaLocalDecl (declName : Name) (fvarId : FVarId) : TacticM Unit := do
+def deltaLocalDecl (declNames : Array Name) (fvarId : FVarId) : TacticM Unit := do
   let mvarId ← getMainGoal
   let localDecl ← fvarId.getDecl
-  let typeNew ← deltaExpand localDecl.type (· == declName)
+  let typeNew ← deltaExpand localDecl.type declNames.contains
   if typeNew == localDecl.type then
-    throwTacticEx `delta mvarId m!"did not delta reduce '{declName}' at '{localDecl.userName}'"
+    throwTacticEx `delta mvarId m!"did not delta reduce '{declNames}' at '{localDecl.userName}'"
   replaceMainGoal [← mvarId.replaceLocalDeclDefEq fvarId typeNew]
 
-def deltaTarget (declName : Name) : TacticM Unit := do
+def deltaTarget (declNames : Array Name) : TacticM Unit := do
   let mvarId ← getMainGoal
   let target ← getMainTarget
-  let targetNew ← deltaExpand target (· == declName)
+  let targetNew ← deltaExpand target declNames.contains
   if targetNew == target then
-    throwTacticEx `delta mvarId m!"did not delta reduce '{declName}'"
+    throwTacticEx `delta mvarId m!"did not delta reduce '{declNames}'"
   replaceMainGoal [← mvarId.replaceTargetDefEq targetNew]
 
 /--
-  "delta " ident (location)?
+  "delta " ident,+ (location)?
 -/
 @[builtinTactic Lean.Parser.Tactic.delta] def evalDelta : Tactic := fun stx => do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
+  let args := if stx[1].isIdent then #[stx[1]] else stx[1].getArgs
+  let declNames ← args.mapM resolveGlobalConstNoOverloadWithInfo
   let loc := expandOptLocation stx[2]
-  withLocation loc (deltaLocalDecl declName) (deltaTarget declName) (throwTacticEx `delta · m!"did not delta reduce '{declName}'")
+  withLocation loc (deltaLocalDecl declNames) (deltaTarget declNames)
+    (throwTacticEx `delta · m!"did not delta reduce '{declNames}'")
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Unfold.lean

@@ -21,7 +21,8 @@ def unfoldTarget (declName : Name) : TacticM Unit := do
 -/
 @[builtinTactic Lean.Parser.Tactic.unfold] def evalUnfold : Tactic := fun stx => do
   let loc := expandOptLocation stx[2]
-  for declNameId in stx[1].getSepArgs do
+  let args := if stx[1][1].isAtom then stx[1].getSepArgs else stx[1].getArgs
+  for declNameId in args do
     go declNameId loc
 where
   go (declNameId : Syntax) (loc : Location) : TacticM Unit := do