[isabelle-dev] A better policy for the typerep class
brianh at cs.pdx.edu
Tue Feb 10 22:45:39 CET 2009
I thought it would be good to clarify my position in a shorter email:
The automatically-generated typerep instances work fine on typedef or
datatype commands, where the instance resides in the same theory as
the type definition.
It is also OK if instances are generated *within Typerep.thy* for all
types defined in earlier theories.
However, if the merging of two theories causes a typerep instance to
be generated, this is *very bad*.
As far as I can tell, Florian would not necessarily disagree with
this. His advice to Amine, recommending to contort his theory
dependencies, has the effect of avoiding theory merges which would
cause typerep instances to be generated.
My advice is to simply disable theory-merge instance generation. This
would be much better than the current workaround, which relies on
carefully preventing this feature from ever being exercised.
If, during a theory merge, the typerep package noticed a missing
instance, printing an error message would actually be more helpful
than the current behavior.
More information about the isabelle-dev