[isabelle-dev] Countable instantiation addition

Alexander Krauss 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...)

Alex



More information about the isabelle-dev mailing list