library fmap: added a comment

1cbcc35a · Jean-Christophe Filliâtre · e2fc9e23 · 1cbcc35a
Commit 1cbcc35a authored Jun 22, 2020 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

stdlib/fmap.mlw stdlib/fmap.mlw +2 -0

No files found.
--- a/stdlib/fmap.mlw
+++ b/stdlib/fmap.mlw
@@ -110,6 +110,8 @@ module MapApp

  type key

+  (* we enforce type `key` to have a decidable equality
+     by requiring the following function *)
  val eq (x y: key) : bool
    ensures { result <-> x = y }