# How to describe the set of “all computable functions” using Coq?

Would the set of all computable functions be just the set of all maps of the form

f : forall n : nat, P n -> nat


where 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?

The usual definition of partial recursive functions using Turing machines and classical logic (with a few novelties) has been implemented in Coq: see

Zammit, Vincent (1997) A Proof of the S-m-n theorem in Coq. Technical report. University of Kent, The University of Kent, Canterbury, Kent, UK