The whole point of my interleave question was to find a notation, but. I learned so much more in the meantime (except for the notation) :-)
-
-
Replying to @fogus
@fogus One more suggestion, with gratuitous use of constructor overloading in Idris (but no dependent types) http://hpaste.org/837052 replies 0 retweets 1 like -
Replying to @edwinbrady
@edwinbrady@fogus I think you're missing a case there, since your "interleave" is the same as what you'd be forced to write with [(a,b)].1 reply 0 retweets 0 likes -
Replying to @mbrcknl1 reply 0 retweets 0 likes
-
Replying to @edwinbrady
@edwinbrady@mbrcknl I've built Idris, but I'm stuck at "load this example into the console" :-(2 replies 0 retweets 1 like
Replying to @fogus
@fogus until I make it a bit cleverer, you'll need to put it in a file. But yes, it is basically @christopherdone's version (which I missed)
4:48 PM - 8 Mar 2013
0 replies
0 retweets
1 like
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.