Given a program $P$ I can write a new program $f(P)$ that does the following: * Let $k$ be the input for $f(P)$. * Using an unbounded loop, find the first $n_0$ such that $P(n_0)=1$. * If $k=0$, output $n_0$ and stop. * Using a bounded loop, find the largest $i\le \max(n_0, k)$ such that $P(i)=1$. * Output $i$ and stop. So far I have only transformed a program $P$ into a new program $f(P)$ -- even constructivists or intuitionists will agree that my function $f$ is explicitly computable. Now assume that $P$ computes the characteristic function of a recursive set $A$ (and is in particular total and outputs only 0 and 1). Then I claim that (constructively): 1. If $A$ is inhabited (i.e., there is some $n\in A$) then $f(P)$ is again total. 2. Every value $f(P)(k)$ is an element of $A$, i.e., $P(f(P)(k))=1$ for all $k$. 3. The function $f(P)$ is weakly monotone, i.e., $k\le k'$ implies $f(P)(k)\le f(P)(k')$. (I think that "weakly monotone" is not the same as "nondecreasing", constructively, but I assume that you meant "weakly monotone".) 4. Every $x\in A$ is a value of $f(P)$. In fact, $f(P)(x)$ first computes some value $n_0 \le x$, and then the largest $i \le x$ with $P(i)=1$, which is $x$ itself. Note: If there is an increasing enumeration of $A$, then $A$ must be inhabited. I think that being nonempty (i.e., "from $A=\emptyset$ we can get a contradiction") is not enough.