@edwinbrady Is this a known issue?
plusComm : (m,n : Nat) -> m + n = n + m
plusComm = proof
intro m,n
induction m
induction n — BOOM!
@dblhelix induction is experimental and still has issues. I think it's known.
-
-
@edwinbrady Okay, thanks!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.