src/ZF/ex/CoUnit.thy
 author lcp Tue Aug 16 18:58:42 1994 +0200 (1994-08-16) changeset 532 851df239ac8b parent 515 abcc438e7c27 child 810 91c68f74f458 permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
```     1 (*  Title: 	ZF/ex/CoUnit.ML
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 Trivial codatatype definitions, one of which goes wrong!
```
```     7
```
```     8 See discussion in
```
```     9   L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
```
```    10   Report 334,  Cambridge University Computer Laboratory.  1994.
```
```    11 *)
```
```    12
```
```    13 CoUnit = QUniv + "Datatype" +
```
```    14
```
```    15 (*This degenerate definition does not work well because the one constructor's
```
```    16   definition is trivial!  The same thing occurs with Aczel's Special Final
```
```    17   Coalgebra Theorem
```
```    18 *)
```
```    19 consts
```
```    20   counit :: "i"
```
```    21 codatatype
```
```    22   "counit" = Con ("x: counit")
```
```    23
```
```    24
```
```    25 (*A similar example, but the constructor is non-degenerate and it works!
```
```    26   The resulting set is a singleton.
```
```    27 *)
```
```    28
```
```    29 consts
```
```    30   counit2 :: "i"
```
```    31 codatatype
```
```    32   "counit2" = Con2 ("x: counit2", "y: counit2")
```
```    33
```
```    34 end
```