let has_dom (#key:eqtype) (#value:Type) (m:t key value) (dom:S.set key)
  = forall x. contains m x <==> S.mem x dom
let has_dom (#key: eqtype) (#value: Type) (m: t key value) (dom: S.set key) =
forall x. contains m x <==> S.mem x dom
FStar.Map.fsti.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked
FStar.Map.fsti
Prims.eqtype FStar.Map.t FStar.Set.set Prims.l_Forall Prims.l_iff Prims.b2t FStar.Map.contains FStar.Set.mem Prims.logical
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

(**

 @summary FStar.Map provides a polymorphic, partial map from keys to
   values, where keys support decidable equality.

 `m:Map.t key value` is a partial map from `key` to `value`

  A distinctive feature of the library is in its model of partiality.

  A map can be seen as a pair of:
    1. a total map `key -> Tot value`
    2. a set of keys that record the domain of the map

*)
module FStar.Map
module S = FStar.Set

(* Map.t key value: The main type provided by this module *)
val t (key:eqtype) ([@@@strictly_positive] value:Type u#a)
  : Type u#a

(* sel m k : Look up key `k` in map `m` *)
val sel: #key:eqtype -> #value:Type -> t key value -> key -> Tot value

(* upd m k v : A map identical to `m` except mapping `k` to `v` *)
val upd: #key:eqtype -> #value:Type -> t key value -> key -> value -> Tot (t key value)

(* const v : A constant map mapping all keys to `v` *)
val const: #key:eqtype -> #value:Type -> value -> Tot (t key value)

(* domain m : The set of keys on which this partial map is defined *)
val domain: #key:eqtype -> #value:Type -> t key value -> Tot (S.set key)

(* contains m k: Decides if key `k` is in the map `m` *)
val contains: #key:eqtype -> #value:Type -> t key value -> key -> Tot bool

(* concat m1 m2 :
      A map whose domain is the union of the domains of `m1` and `m2`.

      Maps every key `k` in the domain of `m1` to `sel m1 k`
      and all other keys to `sel m2 k`.
*)
val concat: #key:eqtype -> #value:Type -> t key value -> t key value -> Tot (t key value)

(* map_val f m:
      A map whose domain is the same as `m` but all values have
      `f` applied to them.
*)
val map_val: #val1:Type -> #val2:Type -> f:(val1 -> val2) -> #key:eqtype -> t key val1 -> Tot (t key val2)

(* restrict s m:
      Restricts the domain of `m` to (domain m `intersect` s)
*)
val restrict: #key:eqtype -> #value:Type -> S.set key -> t key value -> Tot (t key value)

(* const_on dom v: A defined notion, for convenience
     A partial constant map on dom
*)
let const_on (#key:eqtype) (#value:Type) (dom:S.set key) (v:value)
  : t key value
  = restrict dom (const v)


(* map_literal f: A map that is extensionally equal to the function [f] *)
val map_literal (#k:eqtype) (#v:Type) (f: k -> Tot v)
  : t k v

(* disjoint_dom m1 m2:
      Disjoint domains. TODO: its pattern is biased towards `m1`. Why?
 *)
let disjoint_dom (#key:eqtype) (#value:Type) (m1:t key value) (m2:t key value)
  = forall x.{:pattern (contains m1 x)(* ; (contains m2 x) *)} contains m1 x ==> not (contains m2 x)

(* has_dom m dom: A relational version of the `domain m` function *)
val has_dom : m: FStar.Map.t key value -> dom: FStar.Set.set key -> Prims.logical
m: FStar.Map.t key value -> dom: FStar.Set.set key -> Prims.logical