@paulcc_two Decided to type up the code in the article, I'm getting a unification error when trying trivial on case_one_proof...
-
-
Replying to @bishboria
@bishboria@edwinbrady check the term for case 1 is defined. Might have to move a proof Def (see 'gotcha')2 replies 0 retweets 0 likes -
-
Replying to @bishboria
@bishboria Oh! You need to reduce 'foo' with 'compute' first. My fingers just did that automatically...@paulcc_two2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady@bishboria conv doesn't do iota reduction? Oh.1 reply 0 retweets 0 likes -
Replying to @paulcc_two
@paulcc_two Conversion does, but rewrite doesn't do it automatically.@bishboria2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady ouch (any reason?).@bishboria you need compute then...2 replies 0 retweets 1 like -
Replying to @paulcc_two
@paulcc_two iirc, it was leading to surprises when the reduction wasn't explicit.1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady lego had that equiv tactic? That was handy, esp when used with holes1 reply 0 retweets 0 likes
@paulcc_two Yes, I've been meaning to implement that. Should think about tactics a bit more in general though.
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.