More on this here: https://idris2.readthedocs.io/en/latest/reference/records.html …
-
Show this thread
-
Replying to @edwinbrady @id1660
Interesting, so it's not at all type-directed? The "normal" namespace is decluttered, but wouldn't it be nicer to prevent collisions in the projection namespace as well?
2 replies 0 retweets 0 likes -
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...
2 replies 0 retweets 0 likes -
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...)
-
-
Is this what you got Guillaume on?
2 replies 0 retweets 0 likes -
That is the plan
0 replies 0 retweets 1 like
End of conversation
New conversation -
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.