Re: [isabelle] Two orders / class instantiations
> is it possible to have two class instantiations with two different
> relations for the same type? For example having (set, \subset) p.o.
> and also having (set, \supset) p.o. ? For the moment it seems not,
it is impossible to do so in Isabelle. Type class instantiations must
be unique. It is possible to have two identical instantiations in two
different theories, but then these two theories cannot be merged
together (that is, you can't import from both).
> but how do I proceed if I need both orders in a theorem? Thank you!
There are two solutions here:
1) The standard Haskell trick to introduce a new type, e.g.
datatype 'a reverse = Reverse (get_reverse: 'a)
... and then writing an instance
instance reverse :: (po) po where
2) Use locales instead of type classes, as in e.g. HOL-Algebra. For
reference, see the locale manual, especially Â7.1 which specifically
deals with your use case.
This archive was generated by a fusion of
Pipermail (Mailman edition) and