summaryrefslogtreecommitdiff
path: root/plugins/micromega/mutils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/mutils.ml')
-rw-r--r--plugins/micromega/mutils.ml21
1 files changed, 9 insertions, 12 deletions
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 2dd443f0..b4c6d032 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -66,6 +66,15 @@ let all_sym_pairs f l =
| e::l -> xpairs (pair_with acc e l) l in
xpairs [] l
+let all_pairs f l =
+ let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
+
+ let rec xpairs acc l =
+ match l with
+ | [] -> acc
+ | e::lx -> xpairs (pair_with acc e l) lx in
+ xpairs [] l
+
let rec map3 f l1 l2 l3 =
@@ -285,18 +294,6 @@ struct
else XO (index (n lsr 1))
- let idx n =
- (*a.k.a path_of_int *)
- (* returns the list of digits of n in reverse order with initial 1 removed *)
- let rec digits_of_int n =
- if Int.equal n 1 then []
- else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
- in
- List.fold_right
- (fun b c -> (if b then XI c else XO c))
- (List.rev (digits_of_int n))
- (XH)
-
let z x =
match compare x 0 with
| 0 -> Z0