Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



Andreas wrote:

> Of course, this only works for datatypes for which the size plugin can generate size functions. For example, I have not yet tried whether there is also a size function if the datatype contains finite sets and multisets.

Interesting examples. These actually work, thanks to a hook in the "size" plugin:

HOL$ grep BNF_LFP_Size */*thy
Library/FSet.thy:BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}
Library/Multiset.thy:  BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.