Skip to content

New `seq` operation on maps + consistency tweaks for `seq` operation on sets

Robbert Krebbers requested to merge robbert/map_seq into master

This MR introduces a seq operation on maps, which turns a list x_0; ...; x_n into a map:

{[ i := x_0; ... i+n := x_n ]}

On top of that, I made various improvements to the already existing seq operation on sets:

  • Rename it from seq_set into set_seq. Having _set as a suffix instead of a prefix is inconsistent, see also #24 (closed). This is done as part of !45 (merged) now.
  • Provide set_solver support for set_seq.
  • Make the lemmas for set_seq more consistent w.r.t. those for maps.

Due to the rename, it is not backwards compatible. I'm happy to fix Iris and friends.

Edited by Robbert Krebbers

Merge request reports

Loading