diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2015-04-27 17:35:59 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2015-04-28 18:52:12 +0200 |
| commit | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (patch) | |
| tree | e7ca6d2bb16047debdbc0232519c99a11d9a8d0d /plugins/micromega/mutils.ml | |
| parent | 148cf78a4d85ec56818a8ff00719a775670950b9 (diff) | |
maintenance micromega plugin
- add a nra tactic (similar to nia) for non-linear real arithmetic tactic
- fix a long-standing bug in the reification code
- port to the new proof-engine
Diffstat (limited to 'plugins/micromega/mutils.ml')
| -rw-r--r-- | plugins/micromega/mutils.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index a07cbec68..465c7afce 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 = |