281 fun loose_bvar(Bound i,k) = i >= k |
281 fun loose_bvar(Bound i,k) = i >= k |
282 | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k) |
282 | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k) |
283 | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1) |
283 | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1) |
284 | loose_bvar _ = false; |
284 | loose_bvar _ = false; |
285 |
285 |
|
286 fun loose_bvar1(Bound i,k) = i = k |
|
287 | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) |
|
288 | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1) |
|
289 | loose_bvar1 _ = false; |
286 |
290 |
287 (*Substitute arguments for loose bound variables. |
291 (*Substitute arguments for loose bound variables. |
288 Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi). |
292 Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi). |
289 Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0 |
293 Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0 |
290 and the appropriate call is subst_bounds([b,a], c) . |
294 and the appropriate call is subst_bounds([b,a], c) . |