The Coq mailing list

[delahaye AT jurancon.inria.fr (David Delahaye)]

    Hi Pierre,

>  Coq V7 knows about "zeta"-reduction, which is elimination of "let-in"s
>  But there doesn't seem to exist any flag for this conversion (to use in
> some commands like "Eval Cbv Delta [f] Zeta in <term>".
> 
>  Is this addition unnecessary or planified for the future versions ?

    Currently, "zeta"-reduction is dealt with the delta-reduction as shown in
the following session:

Coq < Goal [x:=O]x=x.
1 subgoal
  
  ============================
   [x:=O]x=x

Unnamed_thm < Cbv Delta.
1 subgoal
  
  ============================
   O=O

    I cannot really answer for Hugo (which introduced this primitive let-in)
but, actually, I think it could be a good idea not to add a new flag for a
reduction which can be essentially seen as delta-reduction (from the user 
point
of view).

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The Coq Project                                  <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[Computers are like air conditioners - they stop working properly when you 
open
 Windows.]