feat: make dot notation be affected by export/open
#6189
Merged
+179
−65
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR changes how generalized field notation ("dot notation") resolves the name of the function, adds a feature where terms such as `x.toString` can resolve as `toString x` as a last resort, and modifies the `Function` dot notation to always use the first explicit argument rather than the first function argument. The new rule is that if `x : S`, then `x.f` resolves the name `S.f` relative to the root namespace (hence it now responds to `export` and `open). Breaking change: aliases now resolve differently. Before, if `x : S`, and `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 field notation (`@x.f`) where `x` could be passed as the wrong argument.
Closes leanprover#3031
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 23, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 23, 2024
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
breaks-mathlib
kmill
changed the title
export/open
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 25, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 25, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR changes how generalized field notation ("dot notation") resolves the function. The new resolution rule is that if
x : S, thenx.fresolves the nameS.frelative to the root namespace (hence it now affected byexportandopen). Breaking change: aliases now resolve differently. Before, ifx : S, and ifS.fis an alias forS'.f, thenx.fwould useS'.fand look for an argument of typeS'. Now, it looks for an argument of typeS, which is more generally useful behavior. Code making use of the old behavior should consider definingSorS'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) wherexcould be passed as the wrong argument. This was not a bug for explicit-mode structure projections.Closes #3031. Addresses the
Functionnamespace issue in #1629.