Re: [isabelle] Proposal: An update to Multiset theory



Hi Florian,

> 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).

Jasmin





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