3 ms·
It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes
by tel 12y ago
It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes forces you to invent lots of new proof terms.
- Ono-Sendai 12y agoIndeed. I suspect that's where a lot of my time will be invested, making the checker better, improving error messages, etc..