#Idris challenge (easy): `(a: Nat) -> (b: Nat) -> (a = b) -> (a + b = a * 2) = ?proof`, in 4 tactics or less
@dblhelix @d_christiansen indeed. Idris tries to be as not clever as possible when it comes to type checking (as distinct from elaboration)
-
-
@edwinbrady@dblhelix yes, with that distinction it's very non-clever. The elaborator is the clever bit.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.