feat: various minor changes to List/Array API

src/Init/Data/Array/Basic.lean

@@ -442,8 +442,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
-@[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
-
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]

src/Init/Prelude.lean

@@ -2829,6 +2829,17 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabi
 instance [Monad m] : [Nonempty α] → Nonempty (m α)
   | ⟨x⟩ => ⟨pure x⟩
 
+/-- A fusion of Haskell's `sequence` and `map`. Used in syntax quotations. -/
+def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m β) : m (Array β) :=
+  let rec loop (i : Nat) (j : Nat) (bs : Array β) : m (Array β) :=
+    dite (LT.lt j as.size)
+      (fun hlt =>
+        match i with
+        | 0           => pure bs
+        | Nat.succ i' => Bind.bind (f (as.get j hlt)) fun b => loop i' (hAdd j 1) (bs.push b))
+      (fun _ => pure bs)
+  loop as.size 0 (Array.mkEmpty as.size)
+
 /--
 A function for lifting a computation from an inner `Monad` to an outer `Monad`.
 Like Haskell's [`MonadTrans`], but `n` does not have to be a monad transformer.

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -50,9 +50,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else
-        let ctx ← Simp.mkContext (config := { dsimp := false })
-        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -45,9 +45,7 @@ where
       go mvarId
     else if let some mvarId ← simpIf? mvarId then
       go mvarId
-    else
-      let ctx ← Simp.mkContext
-      match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+    else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -57,9 +57,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else
-        let ctx ← Simp.mkContext (config := { dsimp := false })
-        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -87,7 +87,7 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
     xs.mapM (·.fvarId!.getUserName)
 
 def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
-  let termArgs? := termArg?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
+  let termArgs? := termArg?s.sequenceMap id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
   let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do

src/Lean/Elab/Quotation.lean

@@ -434,7 +434,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             else mkNullNode contents
           -- We use `no_error_if_unused%` in auxiliary `match`-syntax to avoid spurious error messages,
           -- the outer `match` is checking for unused alternatives
-          `(match ($(discrs).mapM fun
+          `(match ($(discrs).sequenceMap fun
                 | `($contents) => no_error_if_unused% some $tuple
                 | _            => no_error_if_unused% none) with
               | some $resId => $yes

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -198,10 +198,11 @@ def rewriteRulesPass (maxSteps : Nat) : Pass where
     let sevalThms ← getSEvalTheorems
     let sevalSimprocs ← Simp.getSEvalSimprocs
 
-    let simpCtx ← Simp.mkContext
-      (config := { failIfUnchanged := false, zetaDelta := true, maxSteps })
-      (simpTheorems := #[bvThms, sevalThms])
-      (congrTheorems := (← getSimpCongrTheorems))
+    let simpCtx : Simp.Context := {
+      config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
+      simpTheorems := #[bvThms, sevalThms]
+      congrTheorems := (← getSimpCongrTheorems)
+    }
 
     let hyps ← goal.getNondepPropHyps
     let ⟨result?, _⟩ ← simpGoal goal
@@ -282,10 +283,11 @@ def embeddedConstraintPass (maxSteps : Nat) : Pass where
 
       let goal ← goal.tryClearMany duplicates
 
-      let simpCtx ← Simp.mkContext
-        (config := { failIfUnchanged := false, maxSteps })
-        (simpTheorems := relevantHyps)
-        (congrTheorems := (← getSimpCongrTheorems))
+      let simpCtx : Simp.Context := {
+        config := { failIfUnchanged := false, maxSteps }
+        simpTheorems := relevantHyps
+        congrTheorems := (← getSimpCongrTheorems)
+      }
 
       let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := ← goal.getNondepPropHyps)
       let some (_, newGoal) := result? | return none

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

@@ -12,10 +12,11 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 private def getContext : MetaM Simp.Context := do
-  Simp.mkContext
-    (simpTheorems  := {})
-    (congrTheorems := (← getSimpCongrTheorems))
-    (config        := Simp.neutralConfig)
+  return {
+    simpTheorems  := {}
+    congrTheorems := (← getSimpCongrTheorems)
+    config        := Simp.neutralConfig
+  }
 
 partial def matchPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Option (Expr × Array Expr)) :=
   withNewMCtxDepth do
@@ -125,7 +126,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         pure (.occs #[] 0 ids.toList)
       | _ => throwUnsupportedSyntax
     let state ← IO.mkRef occs
-    let ctx := (← getContext).setMemoize (occs matches .all _)
+    let ctx := { ← getContext with config.memoize := occs matches .all _ }
     let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state })
     let subgoals ← match ← state.get with
     | .all #[] | .occs _ 0 _ =>

src/Lean/Elab/Tactic/NormCast.lean

@@ -28,10 +28,8 @@ def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) :=
     unless ← isDefEq a'.expr b'.expr do return none
     a'.mkEqTrans (← b'.mkEqSymm b)
   withReducible do
-    let ctx ← Simp.mkContext
-        (simpTheorems := #[s])
-        (congrTheorems := ← Meta.getSimpCongrTheorems)
-    (go (← Simp.mkDefaultMethods).toMethodsRef ctx).run' {}
+    (go (← Simp.mkDefaultMethods).toMethodsRef
+      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
 
 /-- Proves `a = b` by simplifying using move and squash lemmas. -/
 def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
@@ -193,25 +191,19 @@ def derive (e : Expr) : MetaM Simp.Result := do
   -- step 1: pre-processing of numerals
   let r ← withTrace "pre-processing numerals" do
     let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
-    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
-    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
   -- step 2: casts are moved upwards and eliminated
   let r ← withTrace "moving upward, splitting and eliminating" do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
-    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
-    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
   let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
 
   -- step 3: casts are squashed
   let r ← withTrace "squashing" do
     let simpTheorems := #[← normCastExt.squash.getTheorems]
-    let ctx ← Simp.mkContext
-      (config := config)
-      (simpTheorems := simpTheorems)
-      (congrTheorems := congrTheorems)
-    r.mkEqTrans (← simp r.expr ctx simprocs).1
+    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems } simprocs).1
 
   return r
 
@@ -271,7 +263,7 @@ def evalConvNormCast : Tactic :=
 def evalPushCast : Tactic := fun stx => do
   let { ctx, simprocs, dischargeWrapper } ← withMainContext do
     mkSimpContext (simpTheorems := pushCastExt.getTheorems) stx (eraseLocal := false)
-  let ctx := ctx.setFailIfUnchanged false
+  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
   dischargeWrapper.with fun discharge? =>
     discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
 

src/Lean/Elab/Tactic/Simp.lean

@@ -234,7 +234,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             logException ex
           else
             throw ex
-      return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
+      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
     -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
     -- This affects `addSimpTheorem`.
     if (← read).recover then
@@ -311,11 +311,10 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     simpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let ctx ← Simp.mkContext
-     (config := (← elabSimpConfig stx[1] (kind := kind)))
-     (simpTheorems := #[simpTheorems])
-     congrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) ctx
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
+    config      := (← elabSimpConfig stx[1] (kind := kind))
+    simpTheorems := #[simpTheorems], congrTheorems
+  }
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else
@@ -330,7 +329,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    let ctx := ctx.setSimpTheorems simpTheorems
+    let ctx := { ctx with simpTheorems }
     return { ctx, simprocs, dischargeWrapper }
 
 register_builtin_option tactic.simp.trace : Bool := {

src/Lean/Elab/Tactic/Simpa.lean

@@ -36,9 +36,9 @@ deriving instance Repr for UseImplicitLambdaResult
     let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
-    let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
+    let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
     -- TODO: have `simpa` fail if it doesn't use `simp`.
-    let ctx := ctx.setFailIfUnchanged false
+    let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
     dischargeWrapper.with fun discharge? => do
       let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)

src/Lean/Meta/Tactic/AC/Main.lean

@@ -188,10 +188,12 @@ def post (e : Expr) : SimpM Simp.Step := do
   | e, _ => return Simp.Step.done { expr := e }
 
 def rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId := do
-  let simpCtx ← Simp.mkContext
-      (simpTheorems  := {})
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := Simp.neutralConfig)
+  let simpCtx :=
+    {
+      simpTheorems  := {}
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := Simp.neutralConfig
+    }
   let tgt ← instantiateMVars (← mvarId.getType)
   let (res, _) ← Simp.main tgt simpCtx (methods := { post })
   applySimpResultToTarget mvarId tgt res
@@ -205,10 +207,12 @@ def rewriteUnnormalizedRefl (goal : MVarId) : MetaM Unit := do
 
 def acNfHypMeta (goal : MVarId) (fvarId : FVarId) : MetaM (Option MVarId) := do
   goal.withContext do
-    let simpCtx ← Simp.mkContext
-      (simpTheorems  := {})
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := Simp.neutralConfig)
+    let simpCtx :=
+    {
+      simpTheorems  := {}
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := Simp.neutralConfig
+    }
     let tgt ← instantiateMVars (← fvarId.getType)
     let (res, _) ← Simp.main tgt simpCtx (methods := { post })
     return (← applySimpResultToLocalDecl goal fvarId res false).map (·.snd)

src/Lean/Meta/Tactic/Acyclic.lean

@@ -38,10 +38,7 @@ where
       let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
       let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
       -- TODO: we only need the `sizeOf` simp theorems
-      let ctx ← Simp.mkContext
-         (config := { arith := true })
-         (simpTheorems := #[ (← getSimpTheorems) ])
-      match (← simpTarget hlt.mvarId! ctx {}).1 with
+      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] } {}).1 with
       | some _ => return false
       | none   =>
         let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)

src/Lean/Meta/Tactic/Grind/Preprocessor.lean

@@ -38,10 +38,11 @@ abbrev PreM := ReaderT Context $ StateRefT State GrindM
 def PreM.run (x : PreM α) : GrindM α := do
   let thms ← grindNormExt.getTheorems
   let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
-  let simp ← Simp.mkContext
-    (config := { arith := true })
-    (simpTheorems := #[thms])
-    (congrTheorems := (← getSimpCongrTheorems))
+  let simp : Simp.Context := {
+    config := { arith := true }
+    simpTheorems := #[thms]
+    congrTheorems := (← getSimpCongrTheorems)
+  }
   x { simp, simprocs } |>.run' {}
 
 def simp (_goal : Goal) (e : Expr) : PreM Simp.Result := do

src/Lean/Meta/Tactic/Simp/Attr.lean

@@ -73,10 +73,7 @@ def getSimpTheorems : CoreM SimpTheorems :=
 def getSEvalTheorems : CoreM SimpTheorems :=
   sevalSimpExtension.getTheorems
 
-def Simp.Context.mkDefault : MetaM Context := do
-  mkContext
-    (config := {})
-    (simpTheorems := #[(← Meta.getSimpTheorems)])
-    (congrTheorems := (← Meta.getSimpCongrTheorems))
+def Simp.Context.mkDefault : MetaM Context :=
+  return { config := {}, simpTheorems := #[(← Meta.getSimpTheorems)], congrTheorems := (← Meta.getSimpCongrTheorems) }
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -20,6 +20,18 @@ builtin_initialize congrHypothesisExceptionId : InternalExceptionId ←
 def throwCongrHypothesisFailed : MetaM α :=
   throw <| Exception.internal congrHypothesisExceptionId
 
+/--
+  Helper method for bootstrapping purposes. It disables `arith` if support theorems have not been defined yet.
+-/
+def Config.updateArith (c : Config) : CoreM Config := do
+  if c.arith then
+    if (← getEnv).contains ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq then
+      return c
+    else
+      return { c with arith := false }
+  else
+    return c
+
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
   e.isAppOf ``OfNat.ofNat && e.getAppNumArgs >= 3 && (e.getArg! 1).isRawNatLit
@@ -244,7 +256,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
           s ← s.addTheorem (.fvar x.fvarId!) x
           updated := true
       if updated then
-        withSimpTheorems s f
+        withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
       else
         f
   else if (← getMethods).wellBehavedDischarge then
@@ -451,7 +463,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let m ← getMethods
   let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
   let post := m.dpost >> dsimpReduce
-  withInDSimp do
+  withTheReader Simp.Context (fun ctx => { ctx with inDSimp := true }) do
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 def visitFn (e : Expr) : SimpM Result := do
@@ -646,12 +658,11 @@ where
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
     simpLoop e
 
--- TODO: delete
 @[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
 
 def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
-  let ctx ← ctx.setLctxInitIndices
+  let ctx := { ctx with config := (← ctx.config.updateArith), lctxInitIndices := (← getLCtx).numIndices }
   withSimpContext ctx do
     let (r, s) ← go e methods.toMethodsRef ctx |>.run { stats with }
     trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
@@ -799,7 +810,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
     for fvarId in fvarIdsToSimp do
       let localDecl ← fvarId.getDecl
       let type ← instantiateMVars localDecl.type
-      let ctx := ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId)
+      let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
       let (r, stats') ← simp type ctx simprocs discharge? stats
       stats := stats'
       match r.proof? with
@@ -833,7 +844,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
     let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
-    ctx := ctx.setSimpTheorems simpTheorems
+    ctx := { ctx with simpTheorems }
   match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
   | (none, stats) => return (TacticResultCNM.closed, stats)
   | (some mvarId', stats') =>

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -41,7 +41,7 @@ def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
     let ctx ← getContext
     if ctx.dischargeDepth >= ctx.maxDischargeDepth then
       return .maxDepth
-    else withIncDischargeDepth do
+    else withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
       -- We save the state, so that `UsedTheorems` does not accumulate
       -- `simp` lemmas used during unsuccessful discharging.
       -- We use `withPreservedCache` to ensure the cache is restored after `discharge?`
@@ -446,13 +446,10 @@ def mkSEvalMethods : CoreM Methods := do
     wellBehavedDischarge := true
   }
 
-def mkSEvalContext : MetaM Context := do
+def mkSEvalContext : CoreM Context := do
   let s ← getSEvalTheorems
   let c ← Meta.getSimpCongrTheorems
-  mkContext
-    (simpTheorems := #[s])
-    (congrTheorems := c)
-    (config := { ground := true })
+  return { simpTheorems := #[s], congrTheorems := c, config := { ground := true } }
 
 /--
 Invoke ground/symbolic evaluator from `simp`.

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -43,7 +43,7 @@ private def initEntries : M Unit := do
       let localDecl ← h.getDecl
       let proof  := localDecl.toExpr
       simpThms ← simpThms.addTheorem (.fvar h) proof
-      modify fun s => { s with ctx := s.ctx.setSimpTheorems simpThms }
+      modify fun s => { s with ctx.simpTheorems := simpThms }
       if hsNonDeps.contains h then
         -- We only simplify nondependent hypotheses
         let type ← instantiateMVars localDecl.type
@@ -62,7 +62,7 @@ private partial def loop : M Bool := do
     let ctx := (← get).ctx
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
-    let ctx := ctx.setSimpTheorems simpThmsWithoutEntry
+    let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
     let (r, stats) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (stats := { (← get) with })
     modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
     match r with
@@ -98,7 +98,7 @@ private partial def loop : M Bool := do
         simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew)
         modify fun s => { s with
           modified         := true
-          ctx              := ctx.setSimpTheorems simpThmsNew
+          ctx.simpTheorems := simpThmsNew
           entries[i]       := { entry with type := typeNew, proof := proofNew, id := .other idNew }
         }
   -- simplify target

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -52,7 +52,6 @@ abbrev Cache := SExprMap Result
 abbrev CongrCache := ExprMap (Option CongrTheorem)
 
 structure Context where
-  private mk ::
   config           : Config := {}
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
   maxDischargeDepth : UInt32 := UInt32.ofNatTruncate config.maxDischargeDepth
@@ -104,38 +103,6 @@ structure Context where
   inDSimp : Bool := false
   deriving Inhabited
 
-/--
-Helper method for bootstrapping purposes.
-It disables `arith` if support theorems have not been defined yet.
--/
-private def updateArith (c : Config) : CoreM Config := do
-  if c.arith then
-    if (← getEnv).contains ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq then
-      return c
-    else
-      return { c with arith := false }
-  else
-    return c
-
-def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) : MetaM Context := do
-  let config ← updateArith config
-  return { config, simpTheorems, congrTheorems }
-
-def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
-  { c with simpTheorems }
-
-def Context.setLctxInitIndices (c : Context) : MetaM Context :=
-  return { c with lctxInitIndices := (← getLCtx).numIndices }
-
-def Context.setAutoUnfold (c : Context) : Context :=
-  { c with config.autoUnfold := true }
-
-def Context.setFailIfUnchanged (c : Context) (flag : Bool) : Context :=
-  { c with config.failIfUnchanged := flag }
-
-def Context.setMemoize (c : Context) (flag : Bool) : Context :=
-  { c with config.memoize := flag }
-
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
@@ -191,15 +158,6 @@ instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
-@[inline] def withIncDischargeDepth : SimpM α → SimpM α :=
-  withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 })
-
-@[inline] def withSimpTheorems (s : SimpTheoremsArray) : SimpM α → SimpM α :=
-  withTheReader Context (fun ctx => { ctx with simpTheorems := s })
-
-@[inline] def withInDSimp : SimpM α → SimpM α :=
-  withTheReader Context (fun ctx => { ctx with inDSimp := true })
-
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 

src/Lean/Meta/Tactic/Split.lean

@@ -13,11 +13,12 @@ import Lean.Meta.Tactic.Generalize
 namespace Lean.Meta
 namespace Split
 
-def getSimpMatchContext : MetaM Simp.Context := do
-   Simp.mkContext
-      (simpTheorems   := {})
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := { Simp.neutralConfig with dsimp := false })
+def getSimpMatchContext : MetaM Simp.Context :=
+   return {
+      simpTheorems   := {}
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := { Simp.neutralConfig with dsimp := false }
+   }
 
 def simpMatch (e : Expr) : MetaM Simp.Result := do
   let discharge? ← SplitIf.mkDischarge?

src/Lean/Meta/Tactic/SplitIf.lean

@@ -19,10 +19,11 @@ def getSimpContext : MetaM Simp.Context := do
   s ← s.addConst ``if_neg
   s ← s.addConst ``dif_pos
   s ← s.addConst ``dif_neg
-  Simp.mkContext
-    (simpTheorems  := #[s])
-    (congrTheorems := (← getSimpCongrTheorems))
-    (config        := { Simp.neutralConfig with dsimp := false })
+  return {
+    simpTheorems  := #[s]
+    congrTheorems := (← getSimpCongrTheorems)
+    config        := { Simp.neutralConfig with dsimp := false }
+  }
 
 /--
   Default `discharge?` function for `simpIf` methods.

src/Lean/Meta/Tactic/Unfold.lean

@@ -10,10 +10,11 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-private def getSimpUnfoldContext : MetaM Simp.Context := do
-   Simp.mkContext
-      (congrTheorems := (← getSimpCongrTheorems))
-      (config        := Simp.neutralConfig)
+private def getSimpUnfoldContext : MetaM Simp.Context :=
+   return {
+      congrTheorems := (← getSimpCongrTheorems)
+      config        := Simp.neutralConfig
+   }
 
 def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
   if let some unfoldThm ← getUnfoldEqnFor? declName  then