The Coq mailing list

[Petter Urkedal <paurkedal AT gmail.com>]

On Fri, Dec 3, 2010 at 9:13 PM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> This is easy to solve using what I call the convoy pattern in CPDT
> (http://adam.chlipala.net/cpdt/):
>
> Definition test : ordnatpair -> nat.
>  refine (fun p => match p with
>                 | ordnatpair_intro n m H =>
>                       match n return n <= m -> nat with
>                         | O => fun H => _
>                         | S n' => fun H => _
>                       end H
>                   end).

That worked like a charm also on my real case :-).

> If you're getting into the Coq dependent types business, it's probably worth
> reading more of the book.

I certainly will.

Thanks!