On This Page
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
package unionFind
On This Page
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Module UnionFind.MakeSource
Parameters
module S : sig ... endSignature
The new store is implemented on top of the store provided by the user. This means that any extra operations supported by the underlying store (such as, say, opening and committing a transaction) are applicable to this new store as well.
Operations for creating a new store, creating a new reference, reading and writing a reference, and comparing two references. Two references are considered equal after they have been merged by union.
union f s x y does nothing if the references x and y are equal, and merges them if they are distinct. In the latter case, the new content of the merged reference is computed by applying the user-supplied function f to the original contents of x and y.
On This Page