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 /kernel/univ.ml | |
| 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 'kernel/univ.ml')
0 files changed, 0 insertions, 0 deletions