I've just added codata to Idris, in the hope that people now stop asking if it has codata.
@cayleehogg For now, it compiles codata lazily and refuses to reduce at compile time. I'm aiming to add a productivity check before bedtime.
-
-
@cayleehogg as for coinductive proofs, not yet...
End of conversation
New conversation
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.