feat: make Function generalized field notation more usable#13244
Conversation
This PR changes two aspects of generalized field notation for functions to make it more usable. First, the resolution rules for functions and the `Function` pseudo-structure are the same as for other structures, so now `f.foo` resolves `Function.foo` using the currently open namespaces, and it can be used for defining recursive functions (e.g. `Function.iterate`). Second, generalized field notation for functions has an additional rule that it only matches the first *explicit* function argument, which makes it possible to use dot notation with implicit arguments that are type families. Addresses the `Function.swap` example from issue #1629, and an issue from [Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/generalized.20field.20notation.20vs.20namespaces/near/582689850).
github-actions
Bot
added
the
toolchain-available
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
leanprover-bot
added
the
builds-manual
|
Reference manual CI status:
|
|
Mathlib CI status (docs):
|
mathlib-lean-pr-testing
Bot
added
builds-mathlib
|
Mathlib CI status (docs):
|
| /-! | ||
| # Generalized field notation for functions | ||
|
|
||
| Functions use the `Function` namespace, and they always take the first explicit argument that's a function. |
There was a problem hiding this comment.
Mathlib also has the Pi namespace; would you advocate that it should move things into the Function namespace, or that dot notation should try Pi after Function?
There was a problem hiding this comment.
Great question Eric - I note that Core also uses Pi in a few places (e.g. Pi.instSubsingleton, Pi.instNonempty, Pi.instIhabited) - not sure if these should also be Function.
There was a problem hiding this comment.
(Fundamentally I don't understand the rationale for when one is used and not the other: e.g. Function.dcomp in Mathlib could be Pi.comp quite reasonably.
There was a problem hiding this comment.
@eric-wieser I'm not sure — I think this PR needs some community discussion.
I remember in Lean 3 I had an experimental PR where it would resolve names in the implies, function, forall, and pi namespaces depending on whether it was dependent and whether its type was Prop (e.g. an implication would try all four, a nondependent function would try function and pi, a dependent Prop would try forall and pi, etc.). It's too much complexity though, and it won't work well for terms that are partially elaborated, where you don't know yet if it's dependent or a Prop.
4 participants
This PR changes two aspects of generalized field notation for functions to make it more usable. First, the resolution rules for functions and the
Functionpseudo-structure are the same as for other structures, so nowf.fooresolvesFunction.foousing the currently open namespaces, and it can be used for defining recursive functions (e.g.Function.iterate). Second, generalized field notation for functions has an additional rule that it only matches the first explicit function argument, which makes it possible to use dot notation with implicit arguments that are type families.Addresses the
Function.swapexample from issue #1629, and an issue from Zulip.