Background
I once implemented a datatype representing arbitrary real numbers in Haskell. It labels every real numbers by having a Cauchy sequence converging to it. That will let $\mathbb{R}$ be in the usual topology. I also implemented addition, subtraction, multiplication, and division.
But my teacher said, "This doesn't seem to be a good idea. Since comparison is undecidable here, this doesn't look very practical. In particular, letting division by 0 to fall in an infinite loop doesn't look good."
So I wanted my datatype to extend $\mathbb{Q}$. Since equality comparison of $\mathbb{Q}$ is decidable, $\mathbb{Q}$ is in discrete topology. That means a topology on $\mathbb{R}$ must be finer than the discrete topology on $\mathbb{Q}$.
But, I think I found that, even if I could implement such datatype, it will be impractical.
Proof, step 1
Let $\mathbb{R}$ be finer than $\mathbb{Q}$ in discrete topology. Then $\{0\}$ is open in $\mathbb{R}$. Assume $+ : \mathbb{R}^2 → \mathbb{R}$ is continuous. Then $\{(x,-x): x \in \mathbb{R}\}$ is open in $\mathbb{R}^2$. Since $\mathbb{R}^2$ is in product topology, $\{(x,-x)\}$ is a basis element of $\mathbb{R}^2$ for every $x \in \mathbb{R}$. It follows that $\{x\}$ is a basis element of $\mathbb{R}$ for every $x \in \mathbb{R}$. That is, $\mathbb{R}$ is in discrete topology.
Proof, step 2
Since $\mathbb{R}$ is in discrete topology, $\mathbb{R}$ is computably equality comparable. This is a contradiction, so $+$ is not continuous, and thus not computable.
Question
What is bugging me is the bolded text. It is well-known that every computable function is continuous (Weihrauch 2000, p. 6). Though the analytic definition and the topological definition of continuity coincide in functions from and to Euclidean spaces, $\mathbb{R}$ above is not a Euclidean space. So I'm unsure whether my proof is correct. What is the definition of "continuity" in computable analysis?