SeqToBag

[MamounF]

Hello,

I would find useful to add to the Bag module the following:

SeqToBag(s) ==
[i \in Range(s) |-> Cardinality({ix \in DOMAIN s: s[ix] = i})]

Thanks

Mamoun

[muenchnerkindl]

@MamounF Thank you for the suggestion, I created a PR to add a ToBag operator to the SequencesExt module.

[muenchnerkindl]

The operator was added to module SequencesExt.tla as per your suggestion.