diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 8 | ||||
| -rw-r--r-- | kernel/univ.mli | 3 |
2 files changed, 11 insertions, 0 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index d931626e4d..a9b5115886 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -755,6 +755,10 @@ struct let pr x = str(to_string x) + let is_level = function + | (v, 0) -> true + | _ -> false + let level = function | (v,0) -> Some v | _ -> None @@ -809,6 +813,10 @@ struct | Cons (l, n) when is_nil n -> Some l | _ -> None + let is_level l = match node l with + | Cons (l, n) when is_nil n -> Expr.is_level l + | _ -> false + let level l = match node l with | Cons (l, n) when is_nil n -> Expr.level l | _ -> None diff --git a/kernel/univ.mli b/kernel/univ.mli index 20ee554f18..cc5eedefb5 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -118,6 +118,9 @@ sig val pr : t -> Pp.std_ppcmds (** Pretty-printing *) + val is_level : t -> bool + (** Test if the universe is a level or an algebraic universe. *) + val level : t -> Level.t option (** Try to get a level out of a universe, returns [None] if it is an algebraic universe. *) |