max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

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

Browse source
This commit is contained in:
Scott Morrison 2023-03-29 03:32:39 +11:00 • committed by GitHub
parent 7648ec57b5
commit a45f808da4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Util/Name.lean
View file

@ -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]