The Coq mailing list

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

  Hi,

> Le Thursday 17 May 2001 15:23, vous avez ecrit :
> > 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 ?

  Yes, it works with let-expansion. Let's then define the fact to be
guarded as the fact to be guarded when let's are expanded. It will be
available in the next version.

                                                  Hugo

PS: for a quick fix, just replace the code for "IsLetIn (x,a,b,c)" on
line 666 of file V7/kernel/typeops.ml by

      | IsLetIn (x,a,b,c) -> 
          check_rec_call env n lst (whd_betadeltaiota env sigma t)