@edwinbrady Playing around with #idris am I asking too much from the type checker with this? Want n + m = m +n. https://gist.github.com/4593096
@bishboria Alas, yes, you'll need to provide a proof. It depends on the definition of +, which is by recursion on its first argument
-
-
@edwinbrady that's cool, I hadn't seen it done anywhere and wondered if it would work :)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.