chore: update projection/field access wording

doc/std/naming.md

@@ -48,7 +48,7 @@ theorem List.reverse_sublist : l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂ :=
 
 Notice that the second theorem does not have a hypothesis of type `List.Sublist l` for some `l`, so the name `List.Sublist.reverse_iff` would be incorrect.
 
-The advantage of placing results in a namespace like `List.Sublist` is that it enables generalized projection notation, i.e., given `h : l₁ <+ l₂`,
+The advantage of placing results in a namespace like `List.Sublist` is that it enables generalized field notation, i.e., given `h : l₁ <+ l₂`,
 one can write `h.reverse` to obtain a proof of `l₁.reverse <+ l₂.reverse`. Thinking about which dot notations are convenient can act as a guideline
 for deciding where to place a theorem, and is, on occasion, a good reason to duplicate a theorem into multiple namespaces.
 

src/Init/Classical.lean

@@ -200,7 +200,7 @@ end Classical
 export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
 
 /-- Extract an element from an existential statement, using `Classical.choose`. -/
--- This enables projection notation.
+-- This enables generalized field notation (as seen in `Exists.choose_spec`)
 @[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P
 
 /-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/

src/Init/Core.lean

@@ -1614,7 +1614,7 @@ theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v) :=
 /-! # Prop lemmas -/
 
 /-- *Ex falso* for negation: from `¬a` and `a` anything follows. This is the same as `absurd` with
-the arguments flipped, but it is in the `Not` namespace so that projection notation can be used. -/
+the arguments flipped, but it is in the `Not` namespace so that generalized field notation can be used. -/
 def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
 
 /-- Non-dependent eliminator for `And`. -/

src/Lean/Elab/App.lean

@@ -1383,10 +1383,10 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       match name with
       | .str _ s => if s = fieldName && !name.isInternal then accum.push name else accum
       | _ => accum) #[]
-    let hint := match possibleConstants with
+    let hint := match possibleConstants.qsort (lt := Name.lt) with
       | #[] => MessageData.nil
-      | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
-      | opts => .hint' m!"Consider replacing the field projection with a call to one of the following:\
+      | #[opt] => .hint' m!"Consider replacing the field access `.{fieldName}` with a call to the function `{.ofConstName opt}`."
+      | opts => .hint' m!"Consider replacing the field access with a call to one of the following:\
           {MessageData.joinSep (opts.toList.map (indentD m!"• `{.ofConstName ·}`")) .nil}"
     throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \
       known; cannot resolve field `{fieldName}`" ++ hint)

tests/lean/run/invalid_field_notation_mvar.lean

@@ -10,47 +10,47 @@ error: Invalid field notation: Type of
   f
 is not known; cannot resolve field `n`
 
-Hint: Consider replacing the field projection with a call to one of the following:
-  • `BitVec.DivModArgs.n`
+Hint: Consider replacing the field access with a call to one of the following:
   • `Foo.n`
+  • `BitVec.DivModArgs.n`
 ---
 error: Invalid field notation: Type of
   g
 is not known; cannot resolve field `n`
 
-Hint: Consider replacing the field projection with a call to one of the following:
-  • `BitVec.DivModArgs.n`
+Hint: Consider replacing the field access with a call to one of the following:
   • `Foo.n`
+  • `BitVec.DivModArgs.n`
 ---
 error: Invalid field notation: Type of
   f
 is not known; cannot resolve field `f1`
 
-Hint: Consider replacing the field projection `.f1` with a call to the function `Foo.f1`.
+Hint: Consider replacing the field access `.f1` with a call to the function `Foo.f1`.
 ---
 error: Invalid field notation: Type of
   g
 is not known; cannot resolve field `f2`
 
-Hint: Consider replacing the field projection `.f2` with a call to the function `Foo.f2`.
+Hint: Consider replacing the field access `.f2` with a call to the function `Foo.f2`.
 ---
 error: Invalid field notation: Type of
   h
 is not known; cannot resolve field `f3`
 
-Hint: Consider replacing the field projection `.f3` with a call to the function `Foo.f3`.
+Hint: Consider replacing the field access `.f3` with a call to the function `Foo.f3`.
 ---
 error: Invalid field notation: Type of
   f
 is not known; cannot resolve field `f4`
 
-Hint: Consider replacing the field projection `.f4` with a call to the function `Foo.f4`.
+Hint: Consider replacing the field access `.f4` with a call to the function `Foo.f4`.
 ---
 error: Invalid field notation: Type of
   g
 is not known; cannot resolve field `f5`
 
-Hint: Consider replacing the field projection `.f5` with a call to the function `Foo.f5`.
+Hint: Consider replacing the field access `.f5` with a call to the function `Foo.f5`.
 ---
 error: Invalid field notation: Type of
   h
@@ -75,20 +75,37 @@ error: Invalid field notation: Type of
   x✝
 is not known; cannot resolve field `isWhitespace`
 
-Hint: Consider replacing the field projection `.isWhitespace` with a call to the function `Char.isWhitespace`.
+Hint: Consider replacing the field access `.isWhitespace` with a call to the function `Char.isWhitespace`.
 -/
 #guard_msgs in
 example := (·.isWhitespace)
 
 /--
 error: Invalid field notation: Type of
-  x
-is not known; cannot resolve field `succ`
+  x✝
+is not known; cannot resolve field `all`
 
-Hint: Consider replacing the field projection with a call to one of the following:
-  • `Fin.succ`
-  • `Nat.succ`
-  • `Std.PRange.succ`
+Hint: Consider replacing the field access with a call to one of the following:
+  • `Array.all`
+  • `List.all`
+  • `Nat.all`
+  • `Option.all`
+  • `String.all`
+  • `Subarray.all`
+  • `Vector.all`
+  • `String.Slice.all`
+  • `Substring.Raw.all`
+  • `Lean.Meta.ApplyNewGoals.all`
+  • `Lean.Meta.EtaStructMode.all`
+  • `Lean.Meta.Occurrences.all`
+  • `Lean.Meta.TransparencyMode.all`
+  • `Std.Iterators.Iter.all`
+  • `Std.Iterators.IterM.all`
+  • `Substring.Raw.Internal.all`
+  • `Std.Iterators.IterM.Partial.all`
 -/
 #guard_msgs in
-example := fun x => x.succ
+example := (·.all)
+
+example (α : Type) (p : α → Prop) (e : ∃ a, p a) : p e.choose := by
+  grind