diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /kernel/typeops.mli | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e61d5c399e..65531ed38a 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -94,8 +94,9 @@ val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) val judge_of_case : env -> case_info - -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment + -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment + -> unsafe_judgment array + -> unsafe_judgment (** {6 Type of global references. } *) @@ -128,3 +129,7 @@ val type_of_prim : env -> CPrimitives.t -> types val warn_bad_relevance_name : string (** Allow the checker to make this warning into an error. *) + +val should_invert_case : env -> case_info -> bool +(** We have case inversion exactly when going from irrelevant nonempty + (ie 1 constructor) inductive to relevant type. *) |