Source
- URL: https://x.com/o1lo01ol1o/status/2073412350493753796
- Author: o1lo01ol1o (@o1lo01ol1o)
- Posted: 2026-07-04 14:23:21
Branch
1/ @o1lo01ol1o
@VictorTaelin
Do you allow for non-termination on total functions on codata?
2/ @VictorTaelin
@o1lo01ol1o
no codata yet :(
3/ @o1lo01ol1o
@VictorTaelin
You just use really big counters for services?
4/ @VictorTaelin
@o1lo01ol1o
ah, yes you could, but on V1 you’d just disable termination checking there. I don’t think proving stuff about IO is a big demand, not a priority for V1. we can add support that later
5/ @o1lo01ol1o
@VictorTaelin
Good
Related
- Spine: 2026-07-04-sighs