coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Set of Computable functions in Coq

From: Polina Vinogradova <polina.vino AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Set of Computable functions in Coq
Date: Wed, 15 May 2013 13:39:28 -0400

Hello everybody,

I have a question about defining the set of computable functions in Coq - how can you do it?

It seems that the following article outlines how to do it but if anyone has an idea of how I could find some actual code to define this set, I would love to know.

"A proof of the S-m-n theorem in Coq"

http://kar.kent.ac.uk/21524/

Thank you!

Polina

[Coq-Club] Set of Computable functions in Coq, Polina Vinogradova, 05/15/2013
- Re: [Coq-Club] Set of Computable functions in Coq, Adam Chlipala, 05/15/2013