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; Fri, 7 May 1993 19:49:51 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA29342;
          Fri, 7 May 93 11:40:45 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA29337;
          Fri, 7 May 93 11:40:37 -0700
Received: by grolsch.cs.ubc.ca id AA12888 (5.65c/IDA-1.3.5 
          for info-hol@ted.cs.uidaho.edu); Fri, 7 May 1993 11:40:26 -0700
Date: 7 May 93 11:40 -0700
From: Sreeranga Rajan <sree@cs.ubc.ca>
To: vac <vac@air16.larc.nasa.gov>
Cc: info-hol <info-hol@ted.cs.uidaho.edu>
Message-Id: <1174*sree@cs.ubc.ca>
Subject: Re: concrete type definition

prove_constructors_distinct should do it:

------
#let an = define_type `a_new_type` `the_thing = F_ITEM | S_ITEM | T_ITEM`;;
an = 
|- !e0 e1 e2.
    ?! fn. (fn F_ITEM = e0) /\ (fn S_ITEM = e1) /\ (fn T_ITEM = e2)

#prove_constructors_distinct an;;
|- ~(F_ITEM = S_ITEM) /\ ~(F_ITEM = T_ITEM) /\ ~(S_ITEM = T_ITEM)

------
-Sree