@mjd @david Using a fuel parameter is of course a well established idiom, and very common. What I haven't seen yet is to keep the interface of well-founded recursion but elaborate to primitive recursion on fuel, given that using the measure of well-founded recursion (plus one) works so nicely as the initial fuel. But I am bad at literate review, so me not having seen it does not mean it’s novel.