The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Le Thursday 17 May 2001 15:23, vous avez ?rit :
> Hi all,
>
> Ok, we suppose it comes from the new native "let in"
> construct. Unfortunately, 6.x style could be far more readable,
> sometimes.
>
> Require PolyList.
>
> Inductive foo : Set := bar : (list foo)->foo.
>
> (* 6.3 : ok; 7.0 : error *)
> Fixpoint interp [x:foo] : nat :=
> let f = [l](fold_right plus O (map interp l)) in
> Cases x of
> | (bar l) => (f l)
> end

I *do* agree with you. Moreover, in Ocaml programs one usually does
intensive use of the let construction just for readability reasons, that is, 
just to name intermediate results. Most of Ocaml code looks like that :

let f x1 = 
 let x2 = (f1 x1) in 
 let x3 = (f2 x2) in 
 ......

even if x1 and x2 are used once in the body of f.

If my understanding is good, a let-expansion during the verification of the 
guardedness condition would be sufficient to deal with definitions like that. 
Is that actually true ?

Cheers,
Eduardo Gimenez.