Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 19 May 1993 22:44:52 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA29562;
          Wed, 19 May 93 14:35:41 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA29557; Wed, 19 May 93 14:35:37 -0700
Received: by panther.cs.uidaho.edu id AA06521 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Wed, 19 May 1993 14:35:55 -0700
Date: Wed, 19 May 1993 14:35:55 -0700
From: Chris Toshok <toshok@panther.cs.uidaho.edu>
Message-Id: <199305192135.AA06521@panther.cs.uidaho.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Mutually recursive type definitions in HOL88


Hello,

  I remember seeing some discussion about this topic on this mailing list
some time ago, but I didn't think it would ever apply to my work, so I
skimmed over it without really thinking about it.  Well, due to my
ignorance, I now need to find a way to express the following in HOL88.

let TypeResult_Axiom = define_type `TypeResult`
    `TypeResult = Label                              |
                  Typeerror                          |
                  Welltyped                          |
                  NestedType TypeEnv`;;

let TypeEnv_Axiom = define_type `TypeEnv`
    `TypeEnv = typeenv (string -> TypeResult) | EmptyEnv`;;


Is there any way of expressing the above?

Thanks alot for any help.

====================================================================
Chris Toshok                   |  "malloc() is dead,
                               |   long live cons!" 
toshok@snake.cs.uidaho.edu     |       - a perhaps overly-zealous
                               |         Lisp programmer
====================================================================