|
1478
|
1 |
(* Title: ZF/ex/CoUnit.ML
|
|
515
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
515
|
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 |
|
|
810
|
13 |
CoUnit = Datatype +
|
|
515
|
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
|
|
1401
|
20 |
counit :: i
|
|
515
|
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
|
|
1401
|
30 |
counit2 :: i
|
|
515
|
31 |
codatatype
|
|
|
32 |
"counit2" = Con2 ("x: counit2", "y: counit2")
|
|
|
33 |
|
|
|
34 |
end
|