diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-02 17:17:42 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-02 17:17:42 +0000 |
commit | 12965209478bd99dfbe57f07d5b525e51b903f22 (patch) | |
tree | 36a7f5e4802cd321caf02fed0be8349100be09fb /lib/rtree.mli | |
parent | 8b26fd6ba739d4f49fae99ed764b086022e44b50 (diff) |
Modules dans COQ\!\!\!\!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/rtree.mli')
-rw-r--r-- | lib/rtree.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/rtree.mli b/lib/rtree.mli index 5a34c819e..cb8fe0303 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -23,6 +23,11 @@ val mk_rec : 'a t array -> 'a t array to avoid captures when a tree appears under mk_rec *) val lift : int -> 'a t -> 'a t +val map : ('a -> 'b) -> 'a t -> 'b t + +(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *) +val smartmap : ('a -> 'a) -> 'a t -> 'a t + (* Destructors (recursive calls are expanded) *) val dest_param : 'a t -> int val dest_node : 'a t -> 'a * 'a t array |