Update src/Collections/Maps/Maps.dfy

alex-chew · MikaelMayer · web-flow · commit 433ad7d448eb · 2023-02-15T10:37:04.000-08:00
Co-authored-by: Mikaël Mayer &lt;MikaelMayer@users.noreply.github.com&gt;
diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy
@@ -131,7 +131,7 @@ module {:options "-functionSyntax:4"} Maps {
     forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x']
   }
 
-  /* Map an injective function over the keys of a map, retaining the values. */
+  /* Maps an injective function over the keys of a map, retaining the values. */
   function {:opaque} MapKeys<X(!new), Y, X'>(m: map<X, Y>, f: X --> X'): (m': map<X', Y>)
     reads f.reads
     requires forall x {:trigger f.requires(x)} :: f.requires(x)

Original file line number	Diff line number	Diff line change
`@@ -131,7 +131,7 @@ module {:options "-functionSyntax:4"} Maps {`
`131`	`131`	`forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x']`
`132`	`132`	`}`
`133`	`133`
`134`		`- /* Map an injective function over the keys of a map, retaining the values. */`
	`134`	`+ /* Maps an injective function over the keys of a map, retaining the values. */`
`135`	`135`	`function {:opaque} MapKeys<X(!new), Y, X'>(m: map<X, Y>, f: X --> X'): (m': map<X', Y>)`
`136`	`136`	`reads f.reads`
`137`	`137`	`requires forall x {:trigger f.requires(x)} :: f.requires(x)`