From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/univ.mli | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) (limited to 'kernel/univ.mli') diff --git a/kernel/univ.mli b/kernel/univ.mli index 7aaf2ffe..c926c57b 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -20,7 +20,11 @@ sig val is_small : t -> bool (** Is the universe set or prop? *) - + + val is_prop : t -> bool + val is_set : t -> bool + (** Is it specifically Prop or Set *) + val compare : t -> t -> int (** Comparison function *) @@ -87,6 +91,9 @@ sig val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) + val is_levels : t -> bool + (** Test if the universe is a lub of levels or contains +n's. *) + val level : t -> Level.t option (** Try to get a level out of a universe, returns [None] if it is an algebraic universe. *) @@ -159,8 +166,12 @@ val is_initial_universes : universes -> bool val sort_universes : universes -> universes -(** Adds a universe to the graph, ensuring it is >= Prop. *) -val add_universe : universe_level -> universes -> universes +(** Adds a universe to the graph, ensuring it is >= or > Set. + @raises AlreadyDeclared if the level is already declared in the graph. *) + +exception AlreadyDeclared + +val add_universe : universe_level -> bool -> universes -> universes (** {6 Constraints. } *) @@ -332,6 +343,9 @@ sig (** Keeps the order of the instances *) val union : t -> t -> t + (* the number of universes in the context *) + val size : t -> int + end type universe_context = UContext.t @@ -349,6 +363,7 @@ sig val of_instance : Instance.t -> t val of_set : universe_set -> t + val equal : t -> t -> bool val union : t -> t -> t val append : t -> t -> t -- cgit v1.2.3