Re: [isabelle] Inclusion-minimal sets



I assume on weaker structures it would return some maximal element?

Yes. Perhaps this should then be separate from the "normal" Min/Max, since one would not be able to generate code for Min/Max on non-linear orders due to the non-unique nature of the definition.

Another perhaps less problematic way would be to define the set of /all/ maximal elements w.r.t. an order (perhaps even an order specified as a predicate, not a typeclass) I already have something like this in my formalisation of Social Choice Theory anyway.

Getting /some/ maximal element is then trivial and one has separated the arbitrary choice from the maximality-related stuff.


I have no objection in principle, but they way Max is defined would have
to be reorganized considerably and you should talk to Florian about that.

I guess I'll put it on my queue then.


Manuel




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