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



On 08/01/2016 04:44 PM, Jasmin Blanchette wrote:
> Dear Bertram,
> 
>> I believe multp is the more fundamental of the two predicates; after
>> all, the rest of the theory is mostly concerned with the strict multiset
>> extension. But I was reluctant to drop the existing multeqp predicate in
>> favor of multp.
> 
> I see. I cannot find any use of "multeqp" in the repositories I mentioned in my previous email, except for some occurrences in IsaFoR. But "multeqp" can be implemented more efficiently than "multp" (and these predicates appear to be designed for code generation).

Right, code generation was my only reason to investigate this in the
first place (since we had situations where CeTA timed out while trying
to compare "tiny" -- around 10 elements -- multisets), so that's the
only reason why I went with multeqp instead of multp.

cheers

chris




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