Today's piece on coinduction (and its troubled status in type theory) seems to go on for ever. Here it is:http://pigworker.wordpress.com/2015/01/02/coinduction/ …
-
-
Replying to @pigworker
@edwinbrady@pigworker asks "Agda is, moreover, especially careful to forbid dependent case analysis of coinductive data (is Idris?)"1 reply 0 retweets 0 likes -
Replying to @geophf
@geophf@pigworker It isn't especially careful at the moment. There's not much work been done on codata.3 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady@geophf I'm wondering if you can reproduce the usual subject reduction failure. If you haven't actively prevented it, probably.1 reply 0 retweets 0 likes
Replying to @pigworker
@pigworker I'd expect so, yes. @geophf
1:23 PM - 2 Jan 2015
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.