--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/CoUnit.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,34 @@
+(* Title: ZF/ex/CoUnit.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Trivial codatatype definitions, one of which goes wrong!
+
+See discussion in
+ L C Paulson. A Concrete Final Coalgebra Theorem for ZF Set Theory.
+ Report 334, Cambridge University Computer Laboratory. 1994.
+*)
+
+CoUnit = QUniv + "Datatype" +
+
+(*This degenerate definition does not work well because the one constructor's
+ definition is trivial! The same thing occurs with Aczel's Special Final
+ Coalgebra Theorem
+*)
+consts
+ counit :: "i"
+codatatype
+ "counit" = Con ("x: counit")
+
+
+(*A similar example, but the constructor is non-degenerate and it works!
+ The resulting set is a singleton.
+*)
+
+consts
+ counit2 :: "i"
+codatatype
+ "counit2" = Con2 ("x: counit2", "y: counit2")
+
+end