aboutsummaryrefslogtreecommitdiff
path: root/src/boot/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/boot/util')
-rw-r--r--src/boot/util/common.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/boot/util/common.ml b/src/boot/util/common.ml
index 7a95573c..f9b18246 100644
--- a/src/boot/util/common.ml
+++ b/src/boot/util/common.ml
@@ -380,6 +380,13 @@ let rec list_drop n ls =
else list_drop (n-1) (List.tl ls)
;;
+let rec list_count elem lst =
+ match lst with
+ [] -> 0
+ | h::t when h = elem -> 1 + (list_count elem t)
+ | _::t -> list_count elem t
+;;
+
(*
* Auxiliary pair functions.