I'm busy revising the "How Idris Works" paper. Need to submit soon... Comments would be most welcome! http://edwinb.wordpress.com/2013/02/10/idris-a-general-purpose-dependently-typed-programming-language-design-and-implementation/ …
@mukesh_tiwari No, using the pattern [] refines the second vector's length to O by unification.
-
-
@edwinbrady Thank you!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.