Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <08675-0@swan.cl.cam.ac.uk>; Tue, 16 Jun 1992 14:40:02 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA18106; Tue, 16 Jun 92 06:31:02 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA18101; Tue, 16 Jun 92 06:30:56 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <08462-0@swan.cl.cam.ac.uk>; Tue, 16 Jun 1992 14:31:09 +0100 To: wishnu@nl.ruu.cs Cc: info-hol@edu.uidaho.cs.ted Subject: Re: [Wishnu Prasetya: bad varstruct??] In-Reply-To: Your message of Mon, 15 Jun 92 16:43:55 +0100. <"swan.cl.ca.737:15.05.92.15.44.12"@cl.cam.ac.uk> Date: Tue, 16 Jun 92 14:30:54 +0100 From: John Harrison Message-Id: <"swan.cl.ca.474:16.05.92.13.31.18"@cl.cam.ac.uk> I think the only reason you can't use `new_recursive_definition' is that ltree has *lists* of subtrees, so ltree_Axiom doesn't have the expected form. You don't need to have used `define_type' in order to define functions over the type with `new_recursive_definition'. For instance here is a definition of addition over the naturals: #new_recursive_definition true num_Axiom `add` # "($add 0 n = n) /\ ($add (SUC m) n = SUC($add m n))";; |- (!n. 0 add n = n) /\ (!m n. (SUC m) add n = SUC(m add n)) The theorem `num_Axiom' is the recursion principle for natural numbers, and in fact captures all the Peano axioms. John.