The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi Mathieu,

Thanks for replying so soon.

On Sun, Apr 29, 2012 at 01:38:55PM -0400, Mathieu Boespflug wrote:
> 
> The second branch you wrote above is effectively a dead branch, because
> the pattern in the first branch always matches.

Yes I realised that but I was trying to indicate what I am trying to do.

> I think you meant to
> write something like:
>
 
Thanks for the help. My problem was actually more complex but I have now 
solved it with help from the list.

Cheers,

Bernard


> Require Import EqNat.
> 
> Section Example.
> 
> Variable f : nat -> nat.
> Variable m : nat.
> 
> Fixpoint g (n : nat) : nat :=
>   if eq_nat_decide m n then 2 else f n.
> 
> End Example.
> 
> Hope this helps,
> 
> -- Mathieu