fix: generate deprecation warnings for dot notation (#3969)

Fixes #3270 by moving the deprecation check from
`Lean.Elab.Term.mkConsts` to `Lean.Elab.Term.mkConst`, so
`Lean.Elab.Term.mkBaseProjections`, `.elabAppLValsAux`, `.elabAppFn`,
and `.elabForIn` also hit the check. Not all of these really need to hit
the check, so I'll run `!bench` to see if it's a problem.

src/Init/Data/Array/Subarray.lean

@@ -22,7 +22,7 @@ abbrev Subarray.as (s : Subarray α) : Array α := s.array
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
 @[deprecated Subarray.stop_le_array_size]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray
 

src/Init/Data/BitVec/Lemmas.lean

@@ -897,7 +897,7 @@ theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   apply eq_of_toNat_eq
-  have y_toNat_le := Nat.le_of_lt y.toNat_lt
+  have y_toNat_le := Nat.le_of_lt y.isLt
   rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
     Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 

src/Init/Data/Stream.lean

@@ -94,7 +94,7 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+      some (s.array.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
         { s with start := s.start + 1, start_le_stop := this })
     else
       none

src/Lean/Data/RBTree.lean

@@ -100,7 +100,7 @@ def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp :=
   RBMap.any t (fun a _ => p a)
 
 def subset (t₁ t₂ : RBTree α cmp) : Bool :=
-  t₁.all fun a => (t₂.find? a).toBool
+  t₁.all fun a => (t₂.find? a).isSome
 
 def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
   subset t₁ t₂ && subset t₂ t₁

src/Lean/Elab/Term.lean

@@ -1634,6 +1634,7 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
   Remark: fresh universe metavariables are created if the constant has more universe
   parameters than `explicitLevels`. -/
 def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
+  Linter.checkDeprecated constName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice
   let cinfo ← getConstInfo constName
   if explicitLevels.length > cinfo.levelParams.length then
     throwError "too many explicit universe levels for '{constName}'"
@@ -1645,7 +1646,6 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM E
 private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
-    Linter.checkDeprecated declName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice
     let const ← mkConst declName explicitLevels
     return (const, projs) :: result
 

tests/lean/deprecated.lean

@@ -31,3 +31,9 @@ def f4 (x : Nat) := x + 1
 set_option linter.deprecated false in
 #eval f2 0 + 1
 #eval f4 0 + 1
+
+@[deprecated] def Nat.z (x : Nat) := x + 1
+
+/-- warning: `Nat.z` has been deprecated -/
+#guard_msgs in
+example (n : Nat) : n.z = n + 1 := rfl