The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 21 sep 2004, chris jhons wrote:

> Dear all,
>  
> I want to define the following functions in Coq. Can you tell me how?
>  

This is rather straightforward:

Fixpoint even (n:nat) : bool :=
match n with
  | O => true
  | 1 => false
  | S (S n') => even n'
end.


Eval compute in even (S (S O)).
Eval compute in even (S (S (S O))).

(* even' and odd are mutually recursive: *)

Fixpoint even' (n:nat) : bool :=
match n with
  | O => true
  | S n' => odd n'
end
with odd (n:nat) : bool :=
match n with
  | O => false
  | S n' => even' n'
end
.


Eval compute in even' (S (S O)).
Eval compute in even' (S (S (S O))).


Cheers,

Pierre Courtieu