The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Bernard,

Using [nat_compare] does the job. It maps two natural
numbers to an element of [comparison] which is either
Lt, Eq or Gt (with the obvious semantics).

Cheers,

=============
Require Import Arith.
Variable n : nat.
Variable A : Type.
Variable a b c : A.

Fixpoint test (m: nat):=
 match nat_compare m n with
   | Lt => a (*return something*)
   | Eq => b (* return something *)
   | Gt => c (* return something *)
 end.
=============
--
gallais


On 22 April 2012 19:00, Bernard Hurley 
<bernard AT marcade.biz>
 wrote:
> Hi,
>
> How would I match [m] so that I could write a Fixpoint with the format?
>
> +++++++++++++++++++++++++++++++++++
> Variable n: nat.
>
> Fixpoint test (m: nat):=
>  match m with
>    | (* m less than n *) => (*return something*)
>    | (* m equals n *) => (* return something *)
>    | _ => (* return something *)
>  end.
> +++++++++++++++++++++++++++++++++++
>
> Cheers,
>
> Bernard.
>
>