The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

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.


Jianzhou Zhao a écrit :
> Hi,
>
> 'let-in' is for an inductive type with a single constructor.
> It can also define a function:
>   Definition test : bool := let f := fun _ => true in f 0.
> Can we define a recursive function in this way？
> let rec ... in does not seem to be working.
>
> I have been redefining those OCaml functions in Coq,
> to verify these OCaml programs in Coq. Hopefully,
> the Coq extraction can output similar OCaml code
> from these Coq definitions.
>
> But the local recursion cannot be defined.
> It is also fine to define this recursion on the
> top level, but it must take additional arguments
> to store the closure.  I was wondering if the extraction
> can inline these top-level recursion.
> Does anyone know any better idea for this problem?

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B7
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature