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 11:55:48 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14841; Tue, 8 Sep 92 02:25:25 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from utrhcs.cs.utwente.nl by ted.cs.uidaho.edu (16.6/1.34) id AA14836; Tue, 8 Sep 92 02:25:10 -0700 Received: from perseus.cs.utwente.nl by utrhcs.cs.utwente.nl (4.1/RBCS-2.3mx) id AA04257; Tue, 8 Sep 92 11:23:14 +0200 Received: from utis143.cs.utwente.nl by perseus.cs.utwente.nl (4.1/RBCS-2.0) id AA05987; Tue, 8 Sep 92 11:23:13 +0200 Date: Tue, 8 Sep 92 11:23:13 +0200 From: vdvoort@nl.utwente.cs (Mark van de Voort) Message-Id: <9209080923.AA05987@perseus.cs.utwente.nl> To: info-hol@edu.uidaho.cs.ted Subject: Re: short query In-Reply-To: Mail from 'Sreeranga Rajan ' dated: 7 Sep 92 15:52 -0700 Recently Sree wrote: S> Would there be a formal way to tell the constructors apart from other S> constants? Formally there is a difference between constructors and arbitrary constants. For a constant to be a constructor the following law should hold: !t1 t2. (C1 t1 = C2 t2) = (t1 = t2) /\ (C1 = C2) or equivalently the theorems returned by prove_constructors_distinct and prove_constructors_one_one. S> I haven't found a satisfactory way to separate the type constructors S> from "other" constants. The constructors are introduced in the S> theorem that proves the existence of the type, but other constants S> could also appear in that theorem. I guess this is the crux of your question. However I do not really see what you mean. Why would you want to separate them? Maybe you could simply hold them in an ML variable? Mark.