Skip to content

Multiset set notation

Robbert Krebbers requested to merge robbert/multiset_singleton into master

This MR adds a notation {[ x1 ;+ .. ;+ xn ]} for {{ x1 ]} ⊎ .. ⊎ {{ xn ]}.

Todo:

  • bikeshed about notation
  • port tests in !231 (merged) to new notation

Fixes #100 (closed)

Edited by Robbert Krebbers

Merge request reports