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_set
intoset_seq
. Having_set
as a suffix instead of a prefix is inconsistent, see also #24 (closed). - Provide
set_solver
support forset_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