diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /kernel/sorts.mli | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'kernel/sorts.mli')
| -rw-r--r-- | kernel/sorts.mli | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 6c5ce4df80..c49728b146 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -10,13 +10,15 @@ (** {6 The sorts of CCI. } *) -type family = InProp | InSet | InType +type family = InSProp | InProp | InSet | InType -type t = +type t = private + | SProp | Prop | Set | Type of Univ.Universe.t +val sprop : t val set : t val prop : t val type1 : t @@ -25,6 +27,7 @@ val equal : t -> t -> bool val compare : t -> t -> int val hash : t -> int +val is_sprop : t -> bool val is_set : t -> bool val is_prop : t -> bool val is_small : t -> bool @@ -32,6 +35,7 @@ val family : t -> family val hcons : t -> t +val family_compare : family -> family -> int val family_equal : family -> family -> bool module List : sig @@ -42,6 +46,18 @@ end val univ_of_sort : t -> Univ.Universe.t val sort_of_univ : Univ.Universe.t -> t +val super : t -> t + +(** On binders: is this variable proof relevant *) +type relevance = Relevant | Irrelevant + +val relevance_hash : relevance -> int + +val relevance_equal : relevance -> relevance -> bool + +val relevance_of_sort : t -> relevance +val relevance_of_sort_family : family -> relevance + val debug_print : t -> Pp.t val pr_sort_family : family -> Pp.t |