*To*: Stephan Merz <Stephan.Merz at loria.fr>*Subject*: Re: [isabelle] Fwd: Collections: problems with sets of sets*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Mon, 11 Jul 2011 22:51:30 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at kit.edu>*In-reply-to*: <B189A051-158E-4088-8C79-1FA13E04C2D5@loria.fr>*References*: <4E1A9E09.4080504@kit.edu> <B189A051-158E-4088-8C79-1FA13E04C2D5@loria.fr>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20101125 SUSE/3.0.11 Thunderbird/3.0.11

>> 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. Best, Peter

**Follow-Ups**:**Re: [isabelle] Fwd: Collections: problems with sets of sets***From:*Andreas Lochbihler

**References**:**[isabelle] Fwd: Collections: problems with sets of sets***From:*Stephan Merz

- Previous by Date: Re: [isabelle] Collections: problems with sets of sets
- Next by Date: Re: [isabelle] Fwd: Collections: problems with sets of sets
- Previous by Thread: [isabelle] Fwd: Collections: problems with sets of sets
- Next by Thread: Re: [isabelle] Fwd: Collections: problems with sets of sets
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list