The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

Definition g f m n := if eq_nat_dec n m then 2 else f n.

Using Coq.Arith.Peano_dec


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