The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi all,

If I have a function [f: nat -> nat], It is easy to define a function
that differs at just one point in its domain as in:

++++++++++++++++++++++++++++++++
  Variable f : nat -> nat.

  Fixpoint g (n : nat) : nat :=
    match n with
      | 55 => 2
      | _ => f n
    end.
++++++++++++++++++++++++++++++++

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.
++++++++++++++++++++++++++++++++++

Intuitively, since equality is decidable in [nat], there should be some
way of doing this.

Thanks,

Bernard.