From 589487bbcf4020e94751fe6bf5de3500e40ba961 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Nov 2024 16:11:37 -0800 Subject: [PATCH] feat: add `Context.setConfig` --- src/Lean/Meta/Tactic/Simp/Types.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 5eb059fac687..87f538c10bdd 100644 --- 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 }