src/ZF/ex/Enum.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 11354 9b80fe19407f
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/ex/Enum
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Example of a BIG enumeration type
     7 
     8 Can go up to at least 100 constructors, but it takes nearly 7 minutes...
     9 *)
    10 
    11 Enum = Datatype + 
    12 
    13 consts
    14   enum :: i
    15 
    16 datatype
    17   "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
    18          | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
    19          | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
    20          | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
    21          | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
    22          | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
    23   
    24 end