diff options
Diffstat (limited to 'kernel/sorts.mli')
| -rw-r--r-- | kernel/sorts.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 2750145f1..ff7d138d6 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -24,7 +24,9 @@ val equal : t -> t -> bool val compare : t -> t -> int val hash : t -> int +val is_set : t -> bool val is_prop : t -> bool +val is_small : t -> bool val family : t -> family val hcons : t -> t @@ -35,3 +37,6 @@ module List : sig val mem : family -> family list -> bool val intersect : family list -> family list -> family list end + +val univ_of_sort : t -> Univ.universe +val sort_of_univ : Univ.universe -> t |