Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 19 May 1994 11:12:44 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25138; Thu, 19 May 1994 03:57:07 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA25134; Thu, 19 May 1994 03:56:49 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Thu, 19 May 1994 11:52:29 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <18878-0@i80fs2.ira.uka.de>; Thu, 19 May 1994 11:58:41 +0200 Date: Thu, 19 May 94 11:58:40 EDT From: reetz To: info-hol@leopard.cs.byu.edu Subject: converting hol-types to string in hol90.6 Message-Id: <"i80fs2.ira.880:19.04.94.09.58.43"@ira.uka.de> I wonder about how to convert a hol-type into a string of sml in hol90.6 based on NJ/SML 0.93. For terms, I write: fun term_2_string t = System.PrettyPrint.pp_to_string 80 pp_term t; Now, I would like to have something like: fun type_2_string t = ... As far as I could see, pp_type similar to pp_term exists, but it needs an additional parameter of type :int, which seems to be the ``depth'' of the hol-type, so I would have to have a closer look into the hol-type to convert. Does there exists a simpler solution? :-) Ralf (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research *) (* reetz@informatik.uni-karlsruhe.de society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)