@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 iirc, it was leading to surprises when the reduction wasn't explicit.
-
-
@edwinbrady lego had that equiv tactic? That was handy, esp when used with holes -
@paulcc_two Yes, I've been meaning to implement that. Should think about tactics a bit more in general though.
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.