Sometimes when I say types are first class in Idris, someone (quite reasonably) points out you can't pattern match on them. Well, here we go...https://gist.github.com/edwinb/25cd0449aab932bdf49456d426960fed …
-
-
"It should be okay" should be the abstract of every paper about parametricity, erasure, irrelevance, noninterference, etc etc.
-
I think I misunderstood the question anyway. QTT handles this sort of thing :).
- 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.