The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 8 Apr 2010, Jean-Francois Monin wrote:

> You can, provided P is decidable. Not in 1 step but in x steps:
> just write a search program. Here is a short version.

Or even shorter is to use constructive_indefinite_description_nat from 
Coq.Logic.ConstructiveEpsilon. :)

<http://coq.inria.fr/stdlib/Coq.Logic.ConstructiveEpsilon.html#constructive_indefinite_description_nat>

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''