Re: [isabelle] Some more polishing of the multiset theory



I like the first two and think these are uncontroversial.

I don't really know anything about the multiset ordering so I don't have
any opinions on the third one, but what you propose seems reasonable.

Manuel


On 13/02/2021 10:51, Florian Haftmann wrote:
> Hi all,
> 
> after the current Isabelle release I want to take up some notes for
> things which can still be polished in the multiset theory.
> 
> I want to excite feedback especially from those who spent a lot of work
> there in recent times (as far as I remember, Jasmin, beside others).
> 
> 1. Names not following the *_mset convention
> 	* Melem → member_mset
> 	* Mempty → empty_mset
> 
> 2. Names of definitions deviating for historic reasons
> 	* inf_subset_mset → inter_mset
> 	* sup_subset_mset → union_mset
> 
> 3. Names for the multiset ordering
> 	Names mult1 and mult, in a larger setting, are ambiguous.
> 	Possible ideas:
> 	* mult1 → multiset_order_step | Multiset.order_step
> 	* mult → multiset_order_rel | Multiset.order_rel
> 	But alternative names must be really convincing to justify such
> 	a transition.
> 
> Cheers,
> 	Florian
> 

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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