The Coq mailing list

[Pierre Casteran <casteran AT labri.u-bordeaux.fr>]

Hello,

 In the reference manual (V7, p 110) it is said that with the Cbv flag,
only
weak reductions are performed (no reductions under a lambda abstraction
for the
arguments of a function call).

Isn't the following dialogue in contradiction with this assertion ?


Definition nop := [f:nat->nat]f.
Definition twice := [f:nat->nat ; n : nat](f (f n)).
Definition plus_3 := [i:nat](S (S (S i))).

Eval Cbv Beta Delta [plus_3 twice] in (nop [n:nat](twice plus_3 (S n))).
 = (nop [n:nat](S (S (S (S (S (S (S n))))))))


Because of the abstraction on n, i expected to get as answer 
the original term unchanged. Perhaps am I missing something ?


Pierre

-- 
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |   
351 Cours de la Liberation        |   
F-33405 TALENCE Cedex             |   
France                            |   
tel : (+ 33) 5 56 84 69 31
fax : (+ 33) 5 56 84 66 69
email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white
space)
www: http://dept-info.labri.u-bordeaux.fr/~casteran