datatype foo = .... deriving countable, finite,
Tobias also mentioned "set_of", "map_of", etc. But since these aren't class instantiations (we have no constructor classes such as "functor"), we end up with the good old generic datatype interpretation (roughly: datatype -> theory -> theory).
So it seems like we simply want named datatype interpretations that are explicitly invoked via "deriving" (stretching the original Haskell notion quite a bit...)
Alex _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
