[Agda] termination example
Serge D. Mechveliani
mechvel at botik.ru
Mon Sep 30 14:25:27 CEST 2013
why the checker does not prove termination of the function
`power' in the attached program?
(about 140 lines in the attached Main.zip).
The last clause of `power' has the first argument
suc (suc (suc cnt)),
and `power' is recursively called in the RHS with the first
cnt'' = suc (suc cnt).
So, the checker must decide that `power' terminates.
But it does not decide.
It this an error in the checker?
Thank you in advance for explanation,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2159 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130930/5d113531/Main.zip
More information about the Agda