I've just added codata to Idris, in the hope that people now stop asking if it has codata.
-
-
Replying to @edwinbrady
@edwinbrady hah! So how is that going to play with totality checking for proofs? Are corecursive proofs supported?1 reply 0 retweets 0 likes -
Replying to @cayleehogg
@cayleehogg For now, it compiles codata lazily and refuses to reduce at compile time. I'm aiming to add a productivity check before bedtime.1 reply 0 retweets 0 likes -
Replying to @cayleehogg
@cayleehogg as for coinductive proofs, not yet...
2:41 PM - 22 Oct 2012
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.