Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 8 Sep 1992 01:00:21 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14612; Mon, 7 Sep 92 15:54:20 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA14605; Mon, 7 Sep 92 15:54:08 -0700 Received: by grolsch.cs.ubc.ca id AA09740 (5.65c/IDA-1.3.5 for info-hol@ted.cs.uidaho.edu); Mon, 7 Sep 1992 15:52:25 -0700 Date: 7 Sep 92 15:52 -0700 From: Sreeranga Rajan To: info-hol@edu.uidaho.cs.ted Message-Id: <606*sree@cs.ubc.ca> Subject: short query I haven't found a satisfactory way to separate the type constructors from "other" constants. The constructors are introduced in the theorem that proves the existence of the type, but other constants could also appear in that theorem. A quick and simple (possible dirty) way that I use is to enforce a naming convention on the theorem name introuced by "define_type". Would there be a formal way to tell the constructors apart from other constants? -Sree (sree@cs.ubc.ca)