The Test.lean file starts with:
import MiniF2F.Minif2fImport
open BigOperators Real Nat Topology
I am wondering whether globally opening Nat is a good idea. Indeed, many problems involve real numbers and opening Nat shadows relevant lemmas. For example, the following lemma:
#check Nat.mul_eq_zero -- Nat.mul_eq_zero {m n : ℕ} : n * m = 0 ↔ n = 0 ∨ m = 0
shadows:
#check mul_eq_zero -- mul_eq_zero.{u_1} {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b = 0 ↔ a = 0 ∨ b = 0
The latter is useful in some problems involving real numbers. Globally opening Nat makes it inaccessible and makes tactics like exact? ineffective in some cases.
The
Test.leanfile starts with:I am wondering whether globally opening
Natis a good idea. Indeed, many problems involve real numbers and openingNatshadows relevant lemmas. For example, the following lemma:shadows:
The latter is useful in some problems involving real numbers. Globally opening
Natmakes it inaccessible and makes tactics likeexact?ineffective in some cases.