Agda is getting do notation https://github.com/agda/agda/blob/master/CHANGELOG.md#syntax …
-
Show this thread
-
The pattern bind syntax is kinda cool! Match a pattern, but if it fails, continue with a completely different path.
2 replies 1 retweet 5 likesShow this thread -
Agda syntax is a bloody masterpiece.
1 reply 4 retweets 14 likesShow this thread -
Replying to @acid2
IIRC pattern-match-and-bind was inspired by similar notation from
@IdrisLang. Good on Agda for stealing our good ideas, we will steal/have stolen their good ones!1 reply 0 retweets 6 likes -
Replying to @jfdm @idrislang
oh cool, I haven't seen Idris's version either :)
1 reply 0 retweets 1 like -
Replying to @acid2 @idrislang
http://idris.readthedocs.io/en/latest/effects/depeff.html … bottom of the page is a decent example. Cannot remember when it was introduce, many many many moons ago.
1 reply 0 retweets 1 like -
1 reply 0 retweets 1 like
In my TFP 2014 paper first, I think. Syntax matters!
1:05 PM - 30 May 2018
0 replies
0 retweets
3 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.