computability - Existence of a basis in constructive vector spaces

As I was trying to review forgotten knowledge on Vector Spaces in
wikipedia, I read that the existence of a basis follows from Zorn
lemma, hence equivalently from the axiom of choice. Actually, the
answer to another question shows that all three are equivalent.

However, my current (amateur) interest in mathematics is oriented
towards constructive mathematics (though I could hardly say I have much
competence for it). The axiom of choice is not constructive, though
I understand that weaker versions of it, such as those proposed in

intuitionistic theories, are constructive. So I assume the same holds for other equivalent statements.

So my question is: what are constructive versions of the existence of a
basis for Vector Spaces?

To make my question more precise, following the first comments, there
could be constraints that are specifically related to the fact that
everything must be computable anyway in a constructive context.

The fact that no one has yet found a basis for the vector space of

continuous functions from $[0,1]\rightarrow \mathbb R$ does not worry
me too much, and I would not mind if existence of a basis for such a
vector space were not considered by the replacement axiom.

But I am more concerned if you consider the
same, but restricted to continuous computable function over computable
reals from $[0,1]_C\rightarrow \mathbb R_C$ (the subscript $C$ is
intended to indicate that only computable numbers are to be considered.
(though I am afraid the situation may be as bad in the computable
case). Computable reals are denumerable. And, as I understand it,

computable mathematics will have to deal only with denumerable sets.