From 25ea5f6fa1893bcaf60bc59c4b1ac080aa516f43 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 2 Jan 2024 14:36:43 -0800
Subject: [PATCH] chore: add default parameter value for `(simprocs :
 Simprocs)`

---
 src/Lean/Meta/Tactic/Simp/Main.lean    | 14 +++++++-------
 src/Lean/Meta/Tactic/Simp/SimpAll.lean |  2 +-
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 850fcb8008..849ba503dc 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -668,7 +668,7 @@ def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods
 end Simp
 open Simp (UsedSimps Simprocs)
 
-def simp (e : Expr) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
+def simp (e : Expr) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
   | none   => Simp.main e ctx usedSimps (methods := Simp.methodsDefault simprocs)
@@ -679,7 +679,7 @@ def dsimp (e : Expr) (ctx : Simp.Context)
   Simp.dsimpMain e ctx usedSimps (methods := Simp.methodsDefault {})
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
+def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   let target ← instantiateMVars (← mvarId.getType)
   let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
@@ -694,7 +694,7 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs)
 /--
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
-def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
+def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
@@ -729,7 +729,7 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
   otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`.
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
-def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
+def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
   let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps
   return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
@@ -762,7 +762,7 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
   else
     applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
-def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
+def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
@@ -770,7 +770,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simp
     let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
     return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
 
-def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
@@ -809,7 +809,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (disch
       throwError "simp made no progress"
     return (some (fvarIdsNew, mvarIdNew), usedSimps)
 
-def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none)
+def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
     (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do
diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
index 88360538e2..4f62f90775 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
@@ -142,7 +142,7 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   mvarId.withContext do
     let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
     if let .some mvarIdNew := r then