Re: [isabelle] converting a multiset to a list

Unless you have very specific and good reasons for doing so, I would advise against this and would recommend to go in the other direction. If you absolutely insist, you can always use "inv multiset_of". Good luck.


Revantha Ramanayake wrote:
Hi, this question concerns multisets as defined in the theory file Multisets in the standard distribution.

It is easy to define the function multiset_of :: " 'a list => 'a multiset " which forms a multiset from a list in the obvious way.

How do I define a function (of type " 'a multiset => 'a list ") that accepts a multiset and returns a list (where each occurrence in the multiset is an occurrence in the list and vice versa) ? I realize that there are many possible output lists. I am interested in obtaining one such list.



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