https://github.com/leanprover/std4/pull/154

Stream: std4

[Scott Morrison]

@François G. Dorais, your PR yesterday to Std adding lots of lemmas in the Nat namespace is now causing countless errors in mathlib4 of the form:

error: stdout:
./././Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean:232:26: error: ambiguous, possible interpretations
  _root_.pow_add : ∀ (a : ?m.239330) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n

  Nat.pow_add : ∀ (a m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
./././Mathlib/Combinatorics/

Is there a plan to address this?

[Scott Morrison]

I see that some lemmas in Std/Data/Nat/Lemmas.lean are protected and others aren't (including all the new lemmas from yesterday), but I don't see the rule.

[Ruben Van de Velde]

It seems a bit unfortunate that we're ending up with a parallel development of a bunch of mathematics specialized to Nat again, though I also don't have a better proposal

[Scott Morrison]

Could we just protect all these lemmas?

[Mario Carneiro]

They should have all been protected

[Mario Carneiro]

the rule is that anything which has an unnamespaced version in mathlib is protected (and possibly some others where such a lemma is likely)

[Scott Morrison]

https://github.com/leanprover/std4/pull/157

[François G. Dorais]

(deleted)