diff options
Diffstat (limited to 'kernel/esubst.ml')
-rw-r--r-- | kernel/esubst.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 0bd7c515c..30c2387ea 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -29,14 +29,14 @@ let el_id = ELID let rec el_shft_rec n = function | ELSHFT(el,k) -> el_shft_rec (k+n) el | el -> ELSHFT(el,n) -let el_shft n el = if n = 0 then el else el_shft_rec n el +let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el (* cross n binders *) let rec el_liftn_rec n = function | ELID -> ELID | ELLFT(k,el) -> el_liftn_rec (n+k) el | el -> ELLFT(n, el) -let el_liftn n el = if n = 0 then el else el_liftn_rec n el +let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el let el_lift el = el_liftn_rec 1 el @@ -73,7 +73,7 @@ type 'a subs = let subs_id i = ESID i -let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s) +let subs_cons(x,s) = if Int.equal (Array.length x) 0 then s else CONS(x,s) let subs_liftn n = function | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *) @@ -81,13 +81,13 @@ let subs_liftn n = function | lenv -> LIFT (n,lenv) let subs_lift a = subs_liftn 1 a -let subs_liftn n a = if n = 0 then a else subs_liftn n a +let subs_liftn n a = if Int.equal n 0 then a else subs_liftn n a let subs_shft = function | (0, s) -> s | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) | (n, s) -> SHIFT (n,s) -let subs_shft (n,a) = if n = 0 then a else subs_shft(n,a) +let subs_shft (n,a) = if Int.equal n 0 then a else subs_shft(n,a) let subs_shift_cons = function (0, s, t) -> CONS(t,s) @@ -99,7 +99,7 @@ let rec is_subs_id = function ESID _ -> true | LIFT(_,s) -> is_subs_id s | SHIFT(0,s) -> is_subs_id s - | CONS(x,s) -> Array.length x = 0 && is_subs_id s + | CONS(x,s) -> Int.equal (Array.length x) 0 && is_subs_id s | _ -> false (* Expands de Bruijn k in the explicit substitution subs |