chore: don't rely on simp calling decide (leanprover/lake#168)

Kha · Jul 17, 2023 · c28a408 · c28a408
1 parent 657ae5f
commit c28a408
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean
@@ -23,7 +23,7 @@ namespace Name
 open Lean.Name
 
 @[simp] protected theorem beq_false (m n : Name) : (m == n) = false ↔ ¬ (m = n) := by
-  rw [← beq_iff_eq m n]; cases m == n <;> simp
+  rw [← beq_iff_eq m n]; cases m == n <;> simp (config := { decide := true })
 
 @[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n := by
   cases n <;> simp [isPrefixOf]