(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) type level = int option (* Interface functions ******************************************************) let infinite = None let finite i = Some i let is_zero xi = xi = (Some 0) let is_infinite xi = xi = None let succ = function | None -> None | Some i -> Some (succ i) let pred = function | None -> None | Some i when i > 0 -> Some (pred i) | _ -> Some 0 let to_string = function | None -> "" | Some i -> string_of_int i