adding the local modifier restricts the scope?

[holtzermann17]

I don't actually get an error in the final line, though Section 6.4 suggests that one should appear:

def nat.dvd (m n : ℕ) : Prop := ∃ k, n = m * k

instance : has_dvd nat := ⟨nat.dvd⟩

section
local attribute [simp]
theorem nat.dvd_refl3 (n : ℕ) : n ∣ n :=
⟨1, by simp⟩

example : 5 ∣ 5 := by simp
end

example : 5 ∣ 5 := by simp

[holtzermann17]

This also applies to the snippet just below that one.

def nat.dvd (m n : ℕ) : Prop := ∃ k, n = m * k

section
def has_dvd_nat : has_dvd nat := ⟨nat.dvd⟩

local attribute [instance] has_dvd_nat

local attribute [simp]
theorem nat.dvd_refl (n : ℕ) : n ∣ n :=
⟨1, by simp⟩

example : 5 ∣ 5 := by simp
end

-- error:
check 5 ∣ 5

(This works without raising any error.)

[avigad]

Indeed, it seems that dvd has moved to the core library after this was written. I'll work on another example.