From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id C5797BC0A for ; Wed, 23 May 2007 08:25:03 +0200 (CEST) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l4N6P3tl018236 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Wed, 23 May 2007 08:25:03 +0200 Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id 263022020D0; Wed, 23 May 2007 08:25:03 +0200 (CEST) Received: from serveur9-10.lri.fr (serveur9-10 [129.175.9.10]) by smtp.lri.fr (Postfix) with ESMTP id 52D5ECED98; Wed, 23 May 2007 08:25:02 +0200 (CEST) Received: from filliatr by serveur9-10.lri.fr with local (Exim 3.36 #1 (Debian)) id 1HqkHO-0008Dp-00; Wed, 23 May 2007 08:25:02 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <18003.56894.913446.961092@serveur9-10.lri.fr> Date: Wed, 23 May 2007 08:25:02 +0200 From: Jean-Christophe Filliatre To: "Lukasz Stafiniak" Cc: "Jon Harrop" , caml-list@yquem.inria.fr Subject: Re: [Caml-list] functions' recursive construction In-Reply-To: <4a708d20705221631x82b6e9ala0cd8b9d83baa959@mail.gmail.com> References: <200705230021.14814.jon@ffconsultancy.com> <4a708d20705221631x82b6e9ala0cd8b9d83baa959@mail.gmail.com> X-Mailer: VM 7.19 under Emacs 21.4.1 X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at concorde with ID 4653DE3F.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 filliatr:01 lri:01 recursive:01 damien:01 lukasz:01 coq:01 fixpoint:01 nat:01 forall:01 forall:01 fixpoint:01 nat:01 wrote:01 wrote:01 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