The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

Chad and Smolka showed me lt_eq_lt_dec and le_gt_dec:
http://coq.inria.fr/stdlib/Coq.Arith.Compare_dec.html

2012/4/22 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.
>> >
>> >