Skip to content

Commit

Permalink
Update src/Collections/Maps/Maps.dfy
Browse files Browse the repository at this point in the history
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
  • Loading branch information
alex-chew and MikaelMayer authored Feb 15, 2023
1 parent 9f1df71 commit 433ad7d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Collections/Maps/Maps.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 433ad7d

Please sign in to comment.