diff options
| author | Pierre-Marie Pédrot | 2020-12-11 18:21:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-11 18:28:05 +0100 |
| commit | cade097ff6e5670b5f4c3ea832b593cf88251fbd (patch) | |
| tree | ee8f0fec90e56a21f6262bcc2b8423b94e1965b6 /clib/cList.mli | |
| parent | 5a77078718c18b05e7ffb1366d6dd9e439ecfc91 (diff) | |
Fast path in tclPROGRESS.
We first check that the list of goals have the same length before trying to
engage into potentially costly equality checks.
Diffstat (limited to 'clib/cList.mli')
| -rw-r--r-- | clib/cList.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |