Last month I found out that there are in fact discontinuous partial functions on ℝ.
For example, on the domain `D` ≝ {`x`:ℝ | `x` < 0 ∨ 0 ≤ `x`} one can define the function `f` where `f`(`x`) = -1 for `x` < 0 and `f`(`x`) = 1 for 0 ≤ `x`. One can prove that this function is discontinuous using the topology of ℝ.

Classically `D` = ℝ, but constructively one can only prove `D` ⊆ ℝ.
For example consider `y` = ∑_{i : ℕ} `a`_{i}2^{-i}
where `a`_{i} = -1 if the `a`_{i}^{th} proof in one’s system proves false, and `a`_{i} = 0 otherwise. It is easy to prove this sum must converge, so `y` ∈ ℝ; however, if one could constructively prove `y` ∈ `D` then one could prove `y` < 0 or one could prove 0 ≤ `y`. In either case the result would mean the system is inconsistent.

I had thought that all partial functions on ℝ were continuous, and rather than use discontinuous functions one would use the functions with the discontinuous points removed. Apparently I was wrong.

Note that the function `f` is continuous using the natural topology of the representatives of its domain. Also note that one cannot prove there are any discontinuous functions whose domain is all of ℝ.