The Collections module

This module includes a variety of submodules that define properties of various collections:

• Sets: functions and lemmas expressing properties of Dafny's set<T> type, such as properties of subsets, unions, and intersections, filtering of sets using predicates, mapping sets to other sets using functions

• Isets: function and lemmas to manipulate isets

• Seqs: functions and lemmas expressing properties of Dafny's seq<T> type, such as properties of subsequences, filtering of sequences, finding elements (i.e., index-of, last-index-of), inserting or removing elements, reversing, repeating or combining (zipping or flattening) sequences, sorting, and conversion to sets.

• Maps: functions and lemmas to manipulate maps

• Imaps: functions and lemmas to manipulate imaps

• Arrays: manipulations of arrays