Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

chore: don't rely on simp calling decide #168

Merged
merged 2 commits into from
Mar 28, 2023
Merged

chore: don't rely on simp calling decide #168

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8303ea7
chore: don't rely on simp calling decide
kim-em Mar 28, 2023
08b2368
just use the config option
kim-em Mar 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Lake/Util/Name.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down