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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and