The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi Gallais,

Thanks, that's great! Thanks for replying so promptly too!

Bernard.

On Sun, Apr 22, 2012 at 07:11:32PM +0100, gallais @ ensl.org wrote:
> 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.
> >
> >