From cd9b1e7690563ee7eae31baf785254e15cdfa4cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 23 May 2024 14:42:44 +0200 Subject: [PATCH] Apply suggestions from code review (doc) Co-authored-by: Jim Fehrle --- doc/sphinx/language/core/inductive.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index bc5d15b81356..24510959323d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -165,8 +165,8 @@ by giving the type of its arguments alone. Automatic Prop lowering +++++++++++++++++++++++ -When an inductive is declared with no explicit sort, it is put in the -smallest sort which does not prevent large elimination (excluding +When an inductive is declared without an explicit sort, it is put in the +smallest sort which permits large elimination (excluding `SProp`). For :ref:`empty and singleton ` types this means they are declared in `Prop`. @@ -179,7 +179,7 @@ types this means they are declared in `Prop`. Disabling this flag prevents inductives with an explicit non-`Prop` type from being lowered to `Prop`. This will become the default in - a future version. Note :flag:`Dependent Proposition Eliminators` to + a future version. Use :flag:`Dependent Proposition Eliminators` to declare the inductive type in `Prop` while preserving compatibility. Depending on universe minimization they may then be declared in