From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id IAA01773 for caml-red; Thu, 12 Oct 2000 08:25:10 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id AAA31135 for ; Thu, 12 Oct 2000 00:43:35 +0200 (MET DST) Received: from localhost.localdomain (jimbo121.zip.com.au [202.7.88.121]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e9BMhVb15039 for ; Thu, 12 Oct 2000 00:43:32 +0200 (MET DST) Received: from ozemail.com.au (IDENT:root@localhost [127.0.0.1]) by localhost.localdomain (8.9.3/8.8.7) with ESMTP id JAA01197; Thu, 12 Oct 2000 09:35:22 +1100 Message-ID: <39E4EB2A.B4A711A1@ozemail.com.au> Date: Thu, 12 Oct 2000 09:35:22 +1100 From: John Max Skaller X-Mailer: Mozilla 4.7 [en] (X11; I; Linux 2.2.12-20 i686) X-Accept-Language: en MIME-Version: 1.0 To: Chet Murthy CC: caml-list@inria.fr Subject: Re: de Bruijn indices References: <200010101729.NAA27342@nautilus-chet.watson.ibm.com> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: weis@pauillac.inria.fr Chet Murthy wrote: > to build a _large_ system (ok, so Coq isn't large by commercial > standards, but by the standards of academic systems it ain't small) Actually, if you multiply the size of Coq by 10, to get the equivalent size for a C/C++ program, it isn't that small by commercial standands either. :-) -- John (Max) Skaller, mailto:skaller@maxtal.com.au 10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850 checkout Vyper http://Vyper.sourceforge.net download Interscript http://Interscript.sourceforge.net