I think the main reason we still haven't introduced the leading `.x` syntax in Lean is that we're not sure whether it should instead have the Swift meaning of "constructor 'x' of expected type". They both seem useful...
-
-
Using ‘.’ to mean constructor?
1 reply 0 retweets 2 likes -
Not my idea - I'd love to hear alternative suggestions! `_.x` kind of comes closer, but it's still a stretch since we never use `_` for namespaces in any other context.
1 reply 0 retweets 0 likes -
So what's the situation here exactly? You want a unified way of handling names in namespaces, but constructors have the extra feature that they can be overloaded based on the type former they are constructing?
1 reply 0 retweets 0 likes -
Nothing directly to do with namespacing, apart from having to write fewer names. If you use `_.x y...` at expected type `C ...`, try `C.x y...` instead. At least that's how I understood the Swift analog ("Implicit Member Expressions") works.
1 reply 0 retweets 0 likes -
What's wrong with straight-up overloading constructors (like, for example, Agda does)?
1 reply 0 retweets 0 likes -
We try to avoid having too many top-level names (opened) in Lean. Code completion after `_.` could be much more specific, for one.
1 reply 0 retweets 1 like -
It feels like this is asking for some very low-level interactive editing, rather than being hostage to fortune of whatever happens to end up in the program text. It'd be cool if code completion could keep up with goals, and then could be asked only for (relevant) constructors.
1 reply 0 retweets 0 likes -
Someone should write a grant about that :). https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/T007265/1 … (Early days yet, though...)
1 reply 0 retweets 1 like -
Is this what you got Guillaume on?
2 replies 0 retweets 0 likes
That is the plan
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.