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 …
We have one of these in the Prelude: the : (0 a : Type) -> a -> a the _ x = x
-
-
This Tweet is unavailable.
-
Yes, it's Quantitative Type Theory, binders have quantities, either 0, 1 or many. So it wasn't even that tricky to add, just a bit fiddly for run time.
- 1 more reply
-
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.