New `seq` operation on maps + consistency tweaks for `seq` operation on sets
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 fromThis is done as part of !45 (merged) now.seq_setintoset_seq. Having_setas a suffix instead of a prefix is inconsistent, see also #24 (closed). - Provide
set_solversupport forset_seq. - Make the lemmas for
set_seqmore 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