The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

> Is it also true that any closed term of type nat reduces to a term of the
form S ... S O

This is the definition of canonicity which I believe Coq has, although I am
never sure about anything when coinductives are involved (Of course axioms
and opaque terms can stop reduction).


> Does it imply that in the empty context it is impossible to define a
> function (nat -> nat) -> nat which maps f to its minimal value?

The existence of such a function would let you produce a mu-minimization
operator and that contradicts the strong normalization of Coq, so lets say
that it's not possible. I think that if you defined the term and its
property as an axiom: You still have a consistent theory though.
-- 
View this message in context: 
http://www.nabble.com/A-not-so-FSet-specific-question-about-destruction-tp25958672p25979327.html
Sent from the Coq mailing list archive at Nabble.com.