2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
17 let rec icm a = function
21 | B.Bind (_, B.Void, t) -> icm (succ a) t
22 | B.Cast (u, t) -> icm (icm a u) t
24 | B.Bind (_, B.Abst (_, _, u), t)
25 | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t
28 let rec iter_bind d = function
30 | B.Abst (r, n, w) -> B.Abst (r, n, iter_term d w)
31 | B.Abbr v -> B.Abbr (iter_term d v)
32 and iter_term d = function
35 | B.LRef (a, i) as t -> if i < d then t else map d a i
36 | B.Cast (w, v) -> B.Cast (iter_term d w, iter_term d v)
37 | B.Appl (x, w, u) -> B.Appl (x, iter_term d w, iter_term d u)
38 | B.Bind (y, b, u) -> B.Bind (y, iter_bind d b, iter_term (succ d) u)
42 let lift_map h _ a i =
43 if i + h >= 0 then B.LRef (a, i + h) else assert false
46 if h = 0 then t else begin
49 G.icm := icm !G.icm t;