Commit 634fc54e authored by charguer's avatar charguer
Browse files

UFPointer_create

parent 97433982
......@@ -420,6 +420,7 @@ Qed.
(** Lemma for link operations: case of nodes that do not
belong to the two components involved. *)
(* TODO: index L a is in fact not needed *)
Lemma repr_update_neq : forall L a b L' x z,
repr L x z ->
index L a ->
......
(* Union-find: array-based implementation,
simplified by omiting the union-by-rank mechanism *)
type node = ref contents
(*
type contents = Root | Link of node
and node = contents ref
*)
and contents = Root | Link of node
type contents = Root | Link of contents ref
type node = contents ref
let create () =
ref Root
......
type node
val create : unit -> node
......@@ -10,4 +9,3 @@ val union : node -> node -> unit
val same : node -> node -> bool
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment