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