The Coq mailing list

[Mathieu Boespflug <mboes AT tweag.net>]

Hi Bernard,

> But is it possible to define a function that differs at an arbitrary
> integer as the following incorrect code is trying to do:
> 
> +++++++++++++++++++++++++++++++++
>   Variable f : nat -> nat.
>   Variable m : nat.
> 
>   Fixpoint g (n : nat) : nat :=
>     match n with
>       | m => 2
>       | _ => f n
>     end.
> ++++++++++++++++++++++++++++++++++

The second branch you wrote above is effectively a dead branch, because
the pattern in the first branch always matches. I think you meant to
write something like:

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