Re: [isabelle] Fwd: Collections: problems with sets of sets

>> A more general solution would be to abstract over the equality operator in the set's locales such that user-defined equalities could be used. However, neither Peter nor me have attempted to do that yet.
However, we know that problem and have already discussed it. I think
that the result was that it is, in principle, possible. The set
implementation would then store custom equals (and hashcode, compare,
etc.) functions,
that have to be specified, e.g. on construction of a set
(empty-operation). The data structure invariant (and the precondition of
the empty-operation) would require that the custom equals, hashcode,
compare, etc functions are sensible.
A default empty-operation, setting the functions to default values (e.g.
op =, op <), would still be possible.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.