Return-Path: 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, 21 Apr 1993 11:14:18 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA19713; Wed, 21 Apr 93 02:55:19 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA19708; Wed, 21 Apr 93 02:55:09 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Wed, 21 Apr 93 10:21:34 BST From: David Shepherd Message-Id: <19259.9304210954@frogland.inmos.co.uk> Subject: Re: Type abbreviations in hol90.5 To: info-hol@ted.cs.uidaho.edu (info-hol mailing list) Date: Wed, 21 Apr 1993 10:54:46 +0100 (BST) In-Reply-To: <199304202122.AA20785@panther.cs.uidaho.edu> from "Chris Toshok" at Apr 20, 93 02:22:58 pm X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 1114 Chris Toshok has said: > How does one go about defining a type abbreviation in hol90? > in hol88 there is new_type_abbrev, but that function doesn't exist > in hol90. I think that the type abbreviation mechanism in hol88 is done by a bit of hackery in the parser which obviously hasn't been duplicated in hol90. In any case, I think type abbreviation is of limited use as it only works in the parser - i.e. it isn't recognised by the pretty printer. e.g. # new_type_abbrev 'state' ":num#num#bool" # "ST:state";; "ST:num#num#bool" : term I think you can do all that you could with new_type_abbrev (and probably more) by using antiquotation on types. e.g. - val state = ty_antiq(==`:num#num#bool`==); - --`ST:^state`--; --`ST:num#num#bool`-- : term -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "They didn't like the rates, they don't like the poll tax, and they won't like the council tax." - Nicholas Ridley