diff options
Diffstat (limited to 'kernel/sorts.ml')
| -rw-r--r-- | kernel/sorts.ml | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 1e4e4e00b4..09c98ca1bc 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -128,6 +128,25 @@ module Hsorts = let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ +(** On binders: is this variable proof relevant *) +type relevance = Relevant | Irrelevant + +let relevance_equal r1 r2 = match r1,r2 with + | Relevant, Relevant | Irrelevant, Irrelevant -> true + | (Relevant | Irrelevant), _ -> false + +let relevance_of_sort_family = function + | InSProp -> Irrelevant + | _ -> Relevant + +let relevance_hash = function + | Relevant -> 0 + | Irrelevant -> 1 + +let relevance_of_sort = function + | SProp -> Irrelevant + | _ -> Relevant + let debug_print = function | SProp -> Pp.(str "SProp") | Prop -> Pp.(str "Prop") |