diff options
| author | coqbot-app[bot] | 2020-12-15 17:43:59 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-15 17:43:59 +0000 |
| commit | f78f812fcba627a913b8c044626df3642ba17c89 (patch) | |
| tree | 12ff463198be130d49a988f9c9bb1d7349a1d3ed /clib | |
| parent | 46c55ced3d1a78f63b3b50fc12d9760663e87e57 (diff) | |
| parent | cade097ff6e5670b5f4c3ea832b593cf88251fbd (diff) | |
Merge PR #13621: Fast path in tclPROGRESS.
Reviewed-by: herbelin
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cList.ml | 6 | ||||
| -rw-r--r-- | clib/cList.mli | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/clib/cList.ml b/clib/cList.ml index 6b13fac48c..d5520aa2b7 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -23,6 +23,7 @@ sig val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val prefix_of : 'a eq -> 'a list -> 'a list -> bool + val same_length : 'a list -> 'b list -> bool val interval : int -> int -> int list val make : int -> 'a -> 'a list val addn : int -> 'a -> 'a list -> 'a list @@ -154,6 +155,11 @@ external cast : 'a cell -> 'a list = "%identity" (** {6 Equality, testing} *) +let rec same_length l1 l2 = match l1, l2 with +| [], [] -> true +| _ :: l1, _ :: l2 -> same_length l1 l2 +| ([], _ :: _) | (_ :: _, []) -> false + let rec compare cmp l1 l2 = if l1 == l2 then 0 else match l1,l2 with diff --git a/clib/cList.mli b/clib/cList.mli index c8e471f989..6c8df88767 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -42,6 +42,9 @@ sig (** [prefix_of eq l1 l2] returns [true] if [l1] is a prefix of [l2], [false] otherwise. It uses [eq] to compare elements *) + val same_length : 'a list -> 'b list -> bool + (** A more efficient variant of [for_all2eq (fun _ _ -> true)] *) + (** {6 Creating lists} *) val interval : int -> int -> int list |