There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
spurious warning on cyclic pure function with termination measure
If a pure function has a _(decreases) clause, there is no reason to give a warning for a cycle in pure function calls. (Indeed, we should only give a warning if there is a cycle of functions, none of which has a measure.) We could leave the warning in when termination checking is turned off via a switch.