This PR introduces the `dotParam` marker to indicate which parameter should be used for generalized field notation ("dot notation"). Example:
```
class A (α : Type _) where
  a : α → Nat

def A.get {α : Type _} [A α] (self : dotParam α) : Nat := a self

structure B where
  b : Nat

instance : A B := ⟨B.b⟩

namespace B
export A (get)
end B

#check fun (b : B) => b.get
-- b.get : Nat
```
The pretty printing code is modified to support the `export`-resolved dot notation introduced in leanprover#6189.

Closes leanprover#1629, closes leanprover#5482

…n-API `export`s" (#5689)

This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.

Closes the already closed #2524

…n-API `export`s" (leanprover#5689)

This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in leanprover#6189 now incentivizes.

Closes the already closed leanprover#2524

This PR changes how generalized field notation ("dot notation") resolves
the function. The new resolution rule is that if `x : S`, then `x.f`
resolves the name `S.f` relative to the root namespace (hence it now
affected by `export` and `open`). Breaking change: aliases now resolve
differently. Before, if `x : S`, and if `S.f` is an alias for `S'.f`,
then `x.f` would use `S'.f` and look for an argument of type `S'`. Now,
it looks for an argument of type `S`, which is more generally useful
behavior. Code making use of the old behavior should consider defining
`S` or `S'` in terms of the other, since dot notation can unfold
definitions during resolution.

This also fixes a bug in explicit-mode generalized field notation
(`@x.f`) where `x` could be passed as the wrong argument. This was not a
bug for explicit-mode structure projections.

Closes leanprover#3031. Addresses the `Function` namespace issue in leanprover#1629.

…n-API `export`s" (leanprover#5689)

This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in leanprover#6189 now incentivizes.

Closes the already closed leanprover#2524