chore: adapt to decide := false in simp

leanprover-community · Oct 23, 2023 · e6d2c12 · e6d2c12
1 parent 9dc4a10
commit e6d2c12
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Aesop/Options/Public.lean b/Aesop/Options/Public.lean
@@ -115,7 +115,7 @@ structure Options where
 /--
 Options which modify the behaviour of the builtin `simp` normalisation rule.
 Extends `Lean.Meta.Simp.ConfigCtx`, so any option declared there is also valid
-here. For example, you can use `aesop (simp_config := { arith := true })` to get
+here. For example, you can use `aesop (simp_options := { arith := true })` to get
 behaviour similar to `simp (config := { arith := true })` (aka `simp_arith`).
 -/
 structure SimpConfig extends Lean.Meta.Simp.ConfigCtx where

diff --git a/Aesop/Search/Expansion/Norm.lean b/Aesop/Search/Expansion/Norm.lean
@@ -377,7 +377,7 @@ partial def normalizeGoalMVar (rs : RuleSet) (normSimpContext : NormSimpContext)
     NormStep.simp rs normSimpContext options mvarsHashSet,
     NormStep.runPostSimpRules options mvars
   ]
-  runNormSteps rs goal options.maxNormIterations normSteps (by simp)
+  runNormSteps rs goal options.maxNormIterations normSteps (by simp (config := { decide := true }))
 
 -- Returns true if the goal was solved by normalisation.
 def normalizeGoalIfNecessary (gref : GoalRef) [Aesop.Queue Q] :