diff options
Diffstat (limited to 'Jennisys/Jennisys/Utils.fs')
| -rw-r--r-- | Jennisys/Jennisys/Utils.fs | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Jennisys/Jennisys/Utils.fs b/Jennisys/Jennisys/Utils.fs index b6d10060..d5251a08 100644 --- a/Jennisys/Jennisys/Utils.fs +++ b/Jennisys/Jennisys/Utils.fs @@ -221,6 +221,23 @@ let rec ListSet idx v lst = fs :: ListSet (idx-1) v rest
| [] -> failwith "index out of range"
+exception KeyAlreadyExists
+
+// =======================================
+/// requires (key |--> value) !in map
+///
+/// ensures ret = map ++ (key |--> value)
+// =======================================
+let MapAddNew key value map =
+ match Map.tryFind key map with
+ | Some(existingValue) ->
+ if existingValue = value then
+ map
+ else
+ raise KeyAlreadyExists
+ | None ->
+ map |> Map.add key value
+
// =======================================
/// ensures: forall k,v ::
/// if k,v in map2 then
|