Update source/pervasive/map.rs

Co-authored-by: Jay Bosamiya <[email protected]>
verus-lang · Jul 27, 2023 · d7ceec6 · d7ceec6
1 parent 92ed84a
commit d7ceec6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/source/pervasive/map.rs b/source/pervasive/map.rs
@@ -338,7 +338,7 @@ impl<K, V> Map<K, V> {
 impl Map<int,int> {
 
     /// Returns `true` if a map is monotonic -- that is, if the mapping between ordered sets 
-    /// preserves the given order 
+    /// preserves the regular `<=` ordering on integers.
     pub open spec fn monotonic(self) -> bool {
         forall |x: int, y: int| self.dom().contains(x) && self.dom().contains(y) && x <= y 
             ==> #[trigger] self[x] <= #[trigger] self[y]