The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Nikhil Swamy wrote:
> 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).