diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-18 14:19:21 +0100 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-18 14:19:21 +0100 |
commit | e4c9dfe7277ec2e2c4b1e40f60044ba4cade8e61 (patch) | |
tree | e6138370f9b1c2e174f9b13bf0f11e4f39aa667e /kernel/names.ml | |
parent | 93c03652fea5914307b0a6b72b7fec6f9aaec305 (diff) |
ADD: Names.Name.is_{anonymous,name}
Two new (trivial) functions were added:
Names.Name.is_anonymous : Names.Name.t -> bool
Names.Name.is_name : Names.Name.t -> bool
They enable us to write a more compact code.
(example: commit "99633f4" in "relation-extraction" module of "coq-contribs").
Diffstat (limited to 'kernel/names.ml')
-rw-r--r-- | kernel/names.ml | 6 |
1 files changed, 6 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 |