@edwinbrady is yesterday's #idris run length encoding example available anywhere? I'd really like to show it to my colleagues
@erikrozendaal xs isn't a type, but a value, so RLE xs -> [type of xs] (A hint rather than an answer as requested. Happy to elaborate :))
-
-
@edwinbrady yes, I was thinking I needed something like "singleton types". List Char is too general, just want the specific xs :) -
@erikrozendaal Aha. Guaranteeing it's the same list is tricky - you could return an equality proof too, perhaps: (xs' ** xs' = xs) - 1 more reply
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.