Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Thu, 14 Jan 1993 23:09:57 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA29951;
          Thu, 14 Jan 93 14:53:36 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from scylla.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA29945;
          Thu, 14 Jan 93 14:53:14 -0800
Received: from sparta.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation) 
          id AA15532; Thu, 14 Jan 93 17:51:27 EST
Date: Thu, 14 Jan 93 17:51:04 EST
From: shb@com.oracorp
Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA07795;
          Thu, 14 Jan 93 17:51:04 EST
Message-Id: <9301142251.AA07795@sparta.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: new_recursive_definition limitation?

It came as an unpleasant surprise that given

  let foo = define_type `foo` `foo = bar0 | bar1 foo foo`;;

and

  new_constant(`f`,":num->num");;

the command

  new_recursive_definition false foo `test1`
  "(test1 bar0 = 1) /\
   (test1 (bar1 f1 f2) = (test1 f1) + (test1 f2))";;

worked fine, but the command

  new_recursive_definition false foo `test2`
  "(test2 f bar0 = 1) /\
   (test2 f (bar1 f1 f2) = (test2 f f1) + (test2 f f2))";;

produced

  evaluation failed     Can't solve recursion equation: Can't derive
existence theorem

I can't confidently tell from the new_recursive_definition manual
entry whether it's supposed to have this limitation or whether I'm
just making some mistake.  Will someone who knows please tell me?

Steve Brackin
ORA