606aeddf06
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 #3031. Addresses the `Function` namespace issue in #1629.
33 lines
786 B
Text
33 lines
786 B
Text
def Set (α : Type) := α → Prop
|
||
|
||
def Set.union (s₁ s₂ : Set α) : Set α :=
|
||
fun a => s₁ a ∨ s₂ a
|
||
|
||
def FinSet (n : Nat) := Set (Fin n)
|
||
|
||
/-!
|
||
The type of `x` is unfolded to find `Set.union`
|
||
-/
|
||
example (x y : FinSet 10) : FinSet 10 :=
|
||
x.union y
|
||
|
||
namespace FinSet
|
||
export Set (union)
|
||
end FinSet
|
||
|
||
/-!
|
||
Since the types are defeq, this alias works:
|
||
-/
|
||
example (x y : FinSet 10) : FinSet 10 :=
|
||
FinSet.union x y
|
||
|
||
/-!
|
||
However, this dot notation fails since there is no `FinSet` argument.
|
||
However, unfolding is the preferred method.
|
||
-/
|
||
/--
|
||
error: invalid field notation, function 'FinSet.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
|
||
-/
|
||
#guard_msgs in
|
||
example (x y : FinSet 10) : FinSet 10 :=
|
||
x.union y
|