diff options
| author | Pierre-Marie Pédrot | 2013-11-07 22:33:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-24 16:14:04 +0200 |
| commit | 3b9fae83567097d53c3560c532865b334c99d59f (patch) | |
| tree | beeff282e4123a2789efa313398ec4be0ac30b6b /kernel/constr.mli | |
| parent | 58349a91a3243f0b382cf74f9c707e7b652a0d43 (diff) | |
Adding a [fold_map] operation on constrs.
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 858af97b68..f2d9ac9f54 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -203,6 +203,10 @@ val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a val map : (constr -> constr) -> constr -> constr +(** Like {!map}, but also has an additional accumulator. *) + +val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr + (** [map_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at |