From 8303ea778539ca36b4aa11be42833f0d489a5355 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 28 Mar 2023 16:45:09 +1100 Subject: [PATCH 1/2] chore: don't rely on simp calling decide --- Lake/Util/Name.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index 631d00e..00be25e 100644 --- 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 <;> decide @[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n := by cases n <;> simp [isPrefixOf] From 08b2368c6881dc296a6e8170e5d25bb8d01c644a Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 28 Mar 2023 16:52:41 +1100 Subject: [PATCH 2/2] just use the config option --- Lake/Util/Name.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index 00be25e..a7c2f88 100644 --- 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 <;> decide + 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]