The Coq mailing list

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

Daniel Schepler wrote:
> ...and you need to use constructive_definite_description to construct 
> induced functions on a quotient type.  So yes, it's probably useless 
> if you need things to be computable at the end.

[constructive_definite_description] is proved as a theorem without 
relying on axioms, so where would the computation problems show up?