The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

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?

-- 
Jianzhou