The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

> > Say I want to write this function (using the same definitions of A, B and 
> > foo
> as below):
> >
> > Definition bar (a:A) (b:B a) : (B a * unit) :=
> >    (b, match a with
> >          | One =>  foo b
> >          | Two =>  tt
> >        end).
> >
> 
> An instance of what I call the convoy pattern in CPDT gives us this version:
> 
> Definition bar (a:A) (b:B a) : (B a * unit) :=
>    (b, match a return B a -> _ with
>          | One => foo
>          | Two => fun _ => tt
>        end b).
> 

Very cool! This does what I want, I think. Thanks much ... I really should 
read your book! : )
-Nik