To answer a question people sometimes ask: https://www.type-driven.org.uk/edwinb/why-is-idris-2-so-much-faster-than-idris-1.html … In which I explain several bad design decisions I made several years ago...
-
Show this thread
-
Replying to @edwinbrady
"This is usable directly by elaborator reflection [...]. Idris 2 takes a much simpler approach, elaborating syntax directly into the core representation." Does this mean we don't have elaboration reflection for meta-programming in Idris2, yet?
1 reply 0 retweets 2 likes
Replying to @DaTwinkDaddy
Not yet but there'll be something, in some form. I want to think about it a bit more first.
1:58 PM - 25 May 2020
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.