Re: [Caml-list] functions' recursive construction

[Jean-Christophe Filliatre <filliatr@lri.fr>]

Damien Lefortier wrote:
 > I try to do a function f which takes one integer argument and returns
 > a function g which returns its nth arguments.
 > 
 > For example f 3 gives g with let g = fun x -> fun y -> fun z -> z ;;

Lukasz Stafiniak wrote:
 > Would this function (or some approximation) be possible in Coq?

Yes, and here it is (0-based instead of 1-based as above):

======================================================================
Fixpoint t (n:nat) : Type := match n with
  | O => forall (A:Set), A -> A
  | S p => forall (A:Set), A -> t p
end.

Fixpoint f  (n:nat) : t n := 
  match n return t n with
  | O => (fun (A:Set) (x:A) => x)
  | S p => (fun (A:Set) (x:A) => f p)
end.

Eval compute in f 2.
= fun (A : Set) (_ : A) (A0 : Set) (_ : A0) (A1 : Set) (x1 : A1) => x1
     : t 2
======================================================================


-- 
Jean-Christophe