We're thinking of replacing the `(= 5)` operator section notation with a more mathy `· = 5`. This both makes parsing easier and less ambiguous (think `(-1)`) and extends naturally to notations of higher arity (`Γ ⊢ · : ·`).
-
Show this thread
-
Relatedly, I'd like to steal Idris' bang notation, but constraining its scope by the surrounding `do` statement, not the surrounding binder. That should make the scope clearer to users (esp in the presence of other macros) and make it possible to implement it via local-expand
1 reply 0 retweets 2 likesShow this thread
Replying to @derKha
Yes, I think Idris has this slightly wrong. It might also be better to constrain by "block", meaning they don't get lifted out of branches of if expressions.
5:45 AM - 2 Nov 2018
0 replies
0 retweets
2 likes
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.