The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Pierre Corbineau wrote:
> There is a way to do it also the syntax is a bit uglier :
>
> Definition add (m:nat) (n:nat):nat  :=
>   let add_n :=
>     fix add_ (m :nat ) :nat :=
>       match m with
>         O => n
>       | S m' => S (add_ m')
>     end
>   in
>   add_n m.

What about this:

Definition add (m:nat) (n:nat):nat  :=
  let fix add_ m :=
      match m with
        O => n
      | S m' => S (add_ m')
      end
  in
  add_ m.

In Coq, there are two kinds of recursive definitions: fixpoints (for 
well-founded inductive types) and cofixpoints (for coinductive types). 
They are quite different typing and reduction behaviour so they have to 
be distinguished. You have "let fix" and "let cofix" notations that are 
syntactic sugar for a local definition of an anonymous fixpoint (exactly 
what Pierre suggested).

Bruno Barras.