The Coq mailing list

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

On Sun, Apr 24, 2011 at 11:16:58AM -0700, Daniel Schepler wrote:
> On Sunday 24 April 2011 05:49:17 Hugo Herbelin wrote:
> 
> > fix Pind2 {struct p}
> > 
> >     := fun P H1 Hind (H:=...) p => match ... with ... end
> >     :
> >     :  forall P, P 1 -> (forall p, P p -> P (Psucc p)) -> forall p, P p
> 
> By this do you mean
> 
> fix Pind2 {struct p}
>   := fun P H1 Hind =>
>   let H:=... in
>   fun p => match ... end
>   : forall P, ...
> ?

Yes, "... (id:=term) ..." in position of bindings (i.e. in the binding
part of a fun or a forall) is the same as a "... let id := term in
..." in the middle of the fun or forall block (see Chapter 1 of the
reference manual).

Hugo Herbelin