@paulcc_two Decided to type up the code in the article, I'm getting a unification error when trying trivial on case_one_proof...
@paulcc_two Conversion does, but rewrite doesn't do it automatically. @bishboria
-
-
@edwinbrady ouch (any reason?).@bishboria you need compute then... -
@paulcc_two iirc, it was leading to surprises when the reduction wasn't explicit. - 2 more replies
New conversation -
-
-
@edwinbrady@bishboria and = is hardwired too? (didn't spot its Def anywhere) -
@paulcc_two It's hardwired in the sense that its definition is in code rather than library, but otherwise it isn't special@bishboria
End of conversation
New conversation -
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.