]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/level.ml
the partial commit continues
[helm.git] / helm / software / helena / src / common / level.ml
index d33c1be662deda6db265f7169c0795b57913cf7f..b10dda06a4b83f30618790322dd2e5459c3bf49f 100644 (file)
@@ -29,7 +29,12 @@ let succ = function
 
 let pred = function
    | None              -> None
-   | Some i when i > 0 -> Some (pred i)
+   | Some i when i > 1 -> Some (pred i)
+   | _                 -> Some 0
+
+let minus n j = match n with
+   | None              -> None
+   | Some i when i > j -> Some (i - j)
    | _                 -> Some 0
 
 let to_string = function