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 …
My current thinking is that if we're matching (a -> b), then on the RHS we have a : Type and b : a -> Type. This fits nicely with how the evaluator and compiler work, at least.
-
-
How is -> defined here? Is it universal quantification or pi? In Mtac we match on function types using exactly the components you describe but one can get away with a : Type and b : Type for the case of implication (which is a special case of universal quantification in Coq).
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.