The standard library Disjoint_Sets_With_Constant_Time_Union api defines access to a standard datastructure useful for partitioning sets.
The Disjoint_Sets_With_Constant_Time_Union api is implemented by the disjoint_sets_with_constant_time_union package.
The Disjoint_Sets_With_Constant_Time_Union api source code is in src/lib/src/disjoint-sets-with-constant-time-union.api.
The above information is manually maintained and may contain errors.
api {
Disjoint_Set X;
make_singleton_disjoint_set : X -> Disjoint_Set(X );
equal : (Disjoint_Set(X ) , Disjoint_Set(X )) -> Bool;
get : Disjoint_Set(X ) -> X;
set : (Disjoint_Set(X ) , X) -> Void;
unify : ((X , X) -> X)
-> (Disjoint_Set(X ) , Disjoint_Set(X )) -> Bool;
union : (Disjoint_Set(X ) , Disjoint_Set(X )) -> Bool;
link : (Disjoint_Set(X ) , Disjoint_Set(X )) -> Bool;
};