[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)
christian.urban at kcl.ac.uk
Sun Aug 4 21:20:11 CEST 2013
On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote:
> ....I.e. everything that is defined by the new package and
> falls into the fragment of the old package can be registered as an old
> datatype benefiting from all the infrastructure built around it (e.g.
> size function, Quickcheck, and other "datatype interpretations").
On the topic of size functions: I found it always odd that
the existing datatype package (however I think this particular
functionality is now provided by the function package) defines
under <datatype_name>.simps "two" definitions of the corresponding
size function. Consider for example
datatype test = A1 | A2 | A3 "test"
> test_size A1 = 0
> test_size A2 = 0
> test_size (A3 ?test) = test_size ?test + Suc 0
> size A1 = 0
> size A2 = 0
> size (A3 ?test) = size ?test + Suc 0
Surely, it would be more uniform to have just the equations for
size, no? Is there any usage for the test_size definitions?
If not, then maybe in the course of updating the datatype
package, this oddity can be eliminated (Nominal needed to work
around it). But I am happy to admit that I might miss something
More information about the isabelle-dev