fixes for leanprover/lean4#6039

leanprover-community · Nov 12, 2024 · 991bacf · 991bacf
1 parent c006467
commit 991bacf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean
@@ -383,7 +383,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
         anyErased := true
   let simpTheoremsArray := simpTheoremsArray'.fst
   let simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size := by
-    simp [simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
+    simp -index only [simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
   let rs := { rs with
     localNormSimpRules, simpTheoremsArray, simpTheoremsArrayNonempty
   }