# HG changeset patch
# User blanchet
# Date 1377756329 -7200
# Node ID d6d813d7e702874207f27f0f2f8e05e9ac9da0e7
# Parent  775b43e72d82f108ca7ad0a0f87792d4494b61d4
documentation ideas

diff -r 775b43e72d82 -r d6d813d7e702 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Aug 29 07:49:54 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Aug 29 08:05:29 2013 +0200
@@ -1123,6 +1123,11 @@
 
 * no direct way to define recursive functions for default values -- but show trick
   based on overloading
+
+* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
+  (for datatype\_compat and prim(co)rec)
+
+* no way to register same type as both data- and codatatype?
 *}
 
 
diff -r 775b43e72d82 -r d6d813d7e702 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 07:49:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 08:05:29 2013 +0200
@@ -149,6 +149,8 @@
 fun co_induct_of (i :: _) = i;
 fun strong_co_induct_of [_, s] = s;
 
+(* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *)
+
 fun register_fp_sugar key fp_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));