Skip to content

Introduce `SingletonMS` class for multiset singletons.

Robbert Krebbers requested to merge robbert/singletonMS into master
  • Define set-like notation {[+ x1; ..; xn ]} for multisets in terms of the new singleton class and disjoint union ⊎.
  • Remove SemiSet instance for multisets.
  • Prove lemmas regarding ∈ and ∉ for multisets since we no longer get the generic versions for sets.
  • Provide SetUnfoldElemOf instances for multisets since we no longer get the generic versions for sets.
  • Prove lemmas new regarding ∈ and ∉ for ∩

Fixes #100 (closed), #98 (closed) and #87 (closed).

This MR is an alternative to !232 (closed).

Merge request reports