package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
doc/coq-core.clib/CMap/Make/index.html
Module CMap.Make
Source
Parameters
module M : Map.OrderedType
Signature
The underlying Map library
include CSig.MapS with type key = M.t with type 'a t = 'a Map.Make(M).t
Same as add
, but expects the key to be present, and thus faster.
Apply the given function to the binding of the given key.
Recover the set of keys defined in the map.
bind f s
transform the set x1; ...; xn
into x1 := f x1; ...; xn := f xn
.
Alias for fold
, to easily track where we depend on fold order.
find_range in_range m
Given a comparison function in_range x
, that tests if x
is below, above, or inside a given range filter_range
returns the submap of m
whose keys are in range. Note that in_range
has to define a continouous range.
update x f m
returns a map containing the same bindings as m
, except for the binding of x
. Depending on the value of y
where y
is f (find_opt x m)
, the binding of x
is added, removed or updated. If y
is None
, the binding is removed if it exists; otherwise, if y
is Some z
then x
is associated to z
in the resulting map. If x
was already bound in m
to a value that is physically equal to z
, m
is returned unchanged (the result of the function is then physically equal to m
).