Would the set of all computable functions be just the set of all maps of the form
f : forall n : nat, P n -> nat
P : nat -> Prop, and
(P n) has a proof whenever
(f n) is defined - so,
n is in the domain of
f. Is this some smaller set of maps actually computable by Coq, or is this what I want?
If not, is there an existing formalization? Using lambda calculus, or combinators K and S, or some basic concept of an algorithm?
Perhaps along with a proof of the Snm theorem - that says this set is enumerable?