I'm unreasonably excited about having implemented enough of the Idris ide-mode in Blodwen to allow this to work. Next, better name generation...pic.twitter.com/dLlsuH8SBP
-
-
-
It'd be more satisfying if it found 'zipWith' for implementing transposeHelper. Maybe I'll come back to that...
Show this thread
End of conversation
New conversation -
-
-
do reverse!
-
That is beyond its abilities, I'm afraid! At least, with the current brute force search...
- 4 more replies
New conversation -
-
-
edwin that's so cool. but why not expand everything when there's only 1 implementation? that'd be even better!!!
-
It would, but that would be a composition of multiple primitive editing steps which I think might be better done at a higher level. It's in the future plans...
- 4 more replies
New conversation -
-
-
can idris or blodwen extract functions defined implicitly? i.e. like in real analysis you have the implicit function theorem, and you have f : x -> y -> z -> h, and you go and define g as f x y z = 0. so then eg with f x y z = x^2+y^2+z^2, g is the function for a unit circle.
-
this is something I've wanted for very long. we started with programming on the rhs, now with fp we can also program on the lhs, but this rejects sides completely and lets you program "in the middle".
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.