The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/15/2013 01:39 PM, Polina Vinogradova wrote:
> I have a question about defining the set of computable functions in 
> Coq - how can you do it?

Is this really the question, or are you interested in how easy it is to 
prove particular theorems under different formalization choices?

Presumably it's fairly trivial to give _a_ definition of the computable 
functions, based on a formalization of Turing machines.