src/ZF/ex/Data.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 11316 b4e71bd751e4
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/ex/Data.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Sample datatype definition.  
     7 It has four contructors, of arities 0-3, and two parameters A and B.
     8 *)
     9 
    10 Data = Datatype +
    11 
    12 consts
    13   data :: [i,i] => i
    14 
    15 datatype
    16   "data(A,B)" = Con0
    17               | Con1 ("a: A")
    18               | Con2 ("a: A", "b: B")
    19               | Con3 ("a: A", "b: B", "d: data(A,B)")
    20 
    21 end