The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Sat, 27 Nov 2004, Wojciech Moczydlowski wrote:

> My question is - why does the last command give this answer, which
> doesn't seem to be reduced enough? I would expect it to evaluate to 20.
>
> Thanks,
>
> Wojtek

At the end of your definition, use the keyword "Defined" instead of "Save, 
and your function will be reducible. By default, bodies of theorems &
lemmas, finished with Qed or Save, are considered "Opaque" and are not 
unfold-able. You can have a look at the reference manual for more 
information about this Opaque/Transparent distinction.

Pierre Letouzey