Interestingly, this is one of the examples in the idris-demos repo. Binary arithmetic is equivalent to unary. https://github.com/idris-hackers/idris-demos/blob/master/Binary/binary-final.idr#L61 …https://twitter.com/mpweiher/status/821005388057378817 …
-
-
Replying to @edwinbrady
We’d have the technology to reduce the proof to one line, if we’d get around to implementing it (Coq+Agda both have it). Clearly we should.
2 replies 2 retweets 5 likes -
-
Replying to @d_christiansen
Ooh, how did the talk go? (It was today wasn’t it?)
2 replies 0 retweets 0 likes -
-
Replying to @d_christiansen
Sounds good. I was at a departmental away day instead today… (“away” meant the other end of St Andrews)
1 reply 0 retweets 0 likes -
Replying to @edwinbrady
would have been nice to see you. Hope the day went well. I plan on screencasting the talk when I get back to Bloomington.
1 reply 0 retweets 3 likes
Replying to @d_christiansen
nice, I look forward to seeing it, if that happens!
11:45 AM - 16 Jan 2017
0 replies
0 retweets
1 like
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.