4 ms·
I see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.
by more_original 12y ago
I see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.
- seanwilson 12y agoAh, I meant that in the sense of, think of an algorithm you want to write, many of them are structurally recursive and they're straightforward to implement in Coq.
- deleted 12y ago[deleted]