search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.75k stars 427 forks source link

feat: make dot notation be affected by `export`/`open` #6189

Closed kmill closed 3 days ago

kmill commented 5 days ago

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.

kmill commented 5 days ago

This almost addresses #5482. If there were the additional features from #1629 (see comments), then declarations could be exported into a different namespace and then be used with different types.

leanprover-community-bot commented 5 days ago

Mathlib CI status (docs):