Re: [isabelle] Proposal: An update to Multiset theory
> There is, however, one point which I don't understand:
>> But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).
> Comparing the two definitions
> it is difficult to see why this should actually be the case.
Indeed. You can forget my comment. I misparsed the emptiness check as the disequality check "M ~= N" in the Huet-Oppen formulation of the multiset extension (cf. less_multiset\<^sub>H\<^sub>O in Multiset_Order.thy).
This archive was generated by a fusion of
Pipermail (Mailman edition) and