feat: add Context.setConfig (#6072)

This PR adds `Lean.Simp.Context.setConfig` function.
leanprover · Nov 14, 2024 · e55b681 · e55b681
1 parent 6313210
commit e55b681
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -121,6 +121,9 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
   let config ← updateArith config
   return { config, simpTheorems, congrTheorems }
 
+def Context.setConfig (context : Context) (config : Config) : Context :=
+  { context with config }
+
 def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
   { c with simpTheorems }