The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon 
roconnor AT theorem.ca:

> I thought mutually recursive functions were only used on mutually
> inductive types.  Am I wrong?
>

The simplest example I know is parity test :

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

But it's true that mutually recursive definitions are the standard
way to define recursors on mutually inductive types (e.g trees and
forests).

Pierre


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.