The Coq mailing list

[Jasper Stein <J.Stein AT cs.ru.nl>]

> 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.

I have always considered this way of indicating Transparency/Opaqueness 
somewhat strange. I expect definitions to be transparent by default, and 
lemmas to be opaque. Moreover after interactive definitions one puts "Qed." 
just out of habit. The resulting opaqueness of the definition has confounded 
me more that once.

Could we not change Coq's default behaviour to reflect this?

Of course we might then add annotations to reverse this behaviour:

Lemma Transparent ...
Definition Opaque ...

Jasper
-- 
The problem with having an open mind is that people toss in garbage