val upd (#k #v: _) (m: t k v) (key: k) (value: v) : t k v
val upd (#k #v: _) (m: t k v) (key: k) (value: v) : t k v
let upd #k #v (m: t k v) (key: k) (value: v) : t k v = 
  FStar.FunctionalExtensionality.on_domain k (fun key' -> if key = key' then value else m key')
module Spec.Map

let op_Hat_Subtraction_Greater = FStar.FunctionalExtensionality.op_Hat_Subtraction_Greater
/
prims.fst.checked FStar.Pervasives.fsti.checked FStar.FunctionalExtensionality.fsti.checked
Spec.Map.fst
m: Spec.Map.t k v -> key: k -> value: v -> Spec.Map.t k v
Prims.eqtype Spec.Map.t FStar.FunctionalExtensionality.on_domain Prims.op_Equality Prims.bool
let upd #k #v (m: t k v) (key: k) (value: v) : t k v =
  
FStar.FunctionalExtensionality.on_domain k (fun key' -> if key = key' then value else m key')