@edwinbrady is yesterday's #idris run length encoding example available anywhere? I'd really like to show it to my colleagues
@erikrozendaal Aha. Guaranteeing it's the same list is tricky - you could return an equality proof too, perhaps: (xs' ** xs' = xs)
-
-
@edwinbrady I didn't get (xs' ** xs' = xs) to work, but this https://gist.github.com/erikrozendaal/7877107#file-rle-idr-L17 … works (using a singleton type)Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.