@paulcc_two Decided to type up the code in the article, I'm getting a unification error when trying trivial on case_one_proof...
@bishboria Oh! You need to reduce 'foo' with 'compute' first. My fingers just did that automatically... @paulcc_two
-
-
@edwinbrady@bishboria conv doesn't do iota reduction? Oh. -
@paulcc_two Conversion does, but rewrite doesn't do it automatically.@bishboria - 4 more replies
New conversation -
-
-
@edwinbrady@paulcc_two here's a gist of the code just to make sure it's ok so far https://gist.github.com/bishboria/5305418 …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.