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