diff options
Diffstat (limited to 'src/Collections.ml')
-rw-r--r-- | src/Collections.ml | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Collections.ml b/src/Collections.ml index 2cb298a7..351b6523 100644 --- a/src/Collections.ml +++ b/src/Collections.ml @@ -184,6 +184,7 @@ module type Set = sig val pp : Format.formatter -> t -> unit val show : t -> string + val pairwise_distinct : elt list -> bool end module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct @@ -218,6 +219,19 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct pp_string "}" let show s = to_string None s + + let pairwise_distinct ls = + let s = ref empty in + let rec check ls = + match ls with + | [] -> true + | x :: ls' -> + if mem x !s then false + else ( + s := add x !s; + check ls') + in + check ls end (** A map where the bindings are injective (i.e., if two keys are distinct, |