This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

functions' recursive construction
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-05-23 (06:25) From: Jean-Christophe Filliatre Subject: Re: [Caml-list] functions' recursive construction
```
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

```