Is it possible to construct non-analytic functions on the real line in constructive analysis? I'm just a curious outsider when it comes to constructive mathematics, but it seems to me that it is not possible to actually construct non-analytic functions. It seems that the classical counterexamples of step functions, absolute value function, and bump functions cannot be defined constructively. Am I correct or is it possible to actually exhibit a non-analytic function?
I would prefer not to assume any choice principles (dependent choice, countable choice etc.).
 A: The absolute value function can certainly be defined for the Cauchy real line or Dedekind real line.
For the Cauchy real line, it's easy: given a sequence $x_n$ send it to $|x_n|.$ This is a well-defined map of Cauchy sequences.
For the Dedekind real line, the lower bounds are any rational $r$ such that $r<x$ or $r<-x,$ and the upper bounds are any rational $r$ such that $x<r$ and $-x<r.$ To show this defines a Dedekind cut we should show it is "located", i.e. for any rationals $a<b,$ either $a$ is a lower bound or $b$ is an upper bound (a sort of limited excluded middle). The interesting case is when $0<a<b.$ Since $x$ is located we know that either $a<x$ or $x<b,$ but also that either $-b<x$ or $x<-a.$ Either of $a<x$ or $x<-a$ imply $a<|x|,$ and in the other cases we have $|x|<b.$
This covers constructive analysis as pioneered by Bishop.

Similarly $f(x)=\begin{cases}0&x\leq 0\\e^{-1/x}&x>0\end{cases}$ can be defined constructively i.e. there is a constructive definition which is classically equivalent to the classical definition. I'll just work with Dedekind cuts.
A rational $r$ is a lower bound of $f(x)$ if $r<0$ or if $r<e^{-1/a}$ for some positive rational $a<x.$ A rational $r$ is an upper bound of $f(x)$ if $r>e^{-1/b}$ for some positive rational $b>x.$
To show $f(x)$ is located, consider a rational interval $a<b.$ If $a<0$ then $a<f(x).$ Otherwise, by continuity of $\exp$ there are rationals $0<a'<b'$ with $a<e^{-1/a'}<e^{-1/b'}<b.$ That's just a statement about rationals so there aren't any constructive subtleties. Since $x$ is located, either $x<b'$ or $a'<x.$ If $x<b'$ then $f(x)<b.$ If $a'<x$ then $a<f(x).$ In all cases we have shown $a<f(x)$ or $f(x)<b$ as required.
A more general construction is that a function on $\mathbb Q$ that is uniformly continuous on bounded sets extends to $\mathbb R.$ The proof is just the usual proof for a metric space completion, though with a bit more care if trying to avoid countable choice.
