# 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)));