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.