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