5 ms·
I didn't say anything that disagrees with that...I was simply trying to give an easy to understand example for how you justify to a computer that a function wil
by seanwilson 12y ago
I didn't say anything that disagrees with that...I was simply trying to give an easy to understand example for how you justify to a computer that a function will always terminate from the perspective of someone who has never used Coq or another theorem prover.
In this context, it's isn't very illuminating to tell a non-Coq user that all Coq functions terminate; formulating your function definition into something that Coq will accept is the difficult part.
- more_original 12y agoI 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]