diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 19:45:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 19:48:55 +0100 |
| commit | 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e (patch) | |
| tree | 9cfec2542b673e85dc04e340db656e8a3a98dc68 /pretyping/retyping.mli | |
| parent | 9348b4e69738c36a49e61a23a75a55c0e51f8fb7 (diff) | |
Adding a variant get_truncation_family_of of get_sort_family_of.
This function returns InProp or InSet for inductive types only when
the inductive type has been explicitly truncated to Prop or
(impredicative) Set.
For instance, singleton inductive types and small (predicative)
inductive types are not truncated and hence in Type.
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index af86df499..6fdde9046 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -31,8 +31,11 @@ val get_type_of : val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> Sorts.t +(* When [truncation_style] is [true], tells if the type has been explicitly + truncated to Prop or (impredicative) Set; in particular, singleton type and + small inductive types, which have all eliminations to Type, are in Type *) val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> Sorts.family + ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment |