The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Randy,

> This function "shift" doesn't compute as I expected, because
> "le_lt_dec" is Opaque in the library.  Of course, this is just one
> lemma; I simply proved it again for myself, making it Transparent.

  As far as le_lt_dec is concerned (and other lemmas from Peano_dec
and Compare_dec), it is transparent in the current cvs version of Coq.

  As far as I know, the question whether a lemma is Opaque or not
results of a compromise between the need for efficiency (transparency
may induces very strong time penalty on type checking) and convenience
for reduction. 

  For which (other) theorems do you expect transparency?

  Hugo