[isabelle-dev] Countable instantiation addition
krauss at in.tum.de
Fri Jul 22 09:36:38 CEST 2011
> 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...)
More information about the isabelle-dev