diff options
| -rw-r--r-- | kernel/names.ml | 6 | ||||
| -rw-r--r-- | kernel/names.mli | 6 |
2 files changed, 12 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 02587bad9..0aa26fb9c 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -82,6 +82,12 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let is_anonymous = function + | Anonymous -> true + | Name _ -> false + + let is_name = not % is_anonymous + let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 | Name id1, Name id2 -> Id.compare id1 id2 diff --git a/kernel/names.mli b/kernel/names.mli index 40f96813f..6380b17fb 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -68,6 +68,12 @@ sig type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + val is_anonymous : t -> bool + (** Return [true] iff a given name is [Anonymous]. *) + + val is_name : t -> bool + (** Return [true] iff a given name is [Name _]. *) + val compare : t -> t -> int (** Comparison over names. *) |