@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@bishboria and = is hardwired too? (didn't spot its Def anywhere)1 reply 0 retweets 0 likes
Replying to @paulcc_two
@paulcc_two It's hardwired in the sense that its definition is in code rather than library, but otherwise it isn't special @bishboria
2:25 PM - 3 Apr 2013
0 replies
0 retweets
0 likes
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.