diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 8de4e7b4ec42..8cac71f341b9 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -513,10 +513,19 @@ where
             accLevelAtCtor ctor ctorParam r rOffset
 
 /--
-Heuristic: we prefer a `Prop` over `Type` if the inductive type could be a syntactic subsingleton.
-However, we prefer `Type` in the following cases:
-- if there are no constructors
-- if each constructor has no parameters
+Decides whether the inductive type should be `Prop`-valued when the universe is not given
+and when the universe inference algorithm `collectUniverses` determines
+that the inductive type could naturally be `Prop`-valued.
+Recall: the natural universe level is the mimimum universe level for all the types of all the constructor parameters.
+
+Heuristic:
+- We want `Prop` when each inductive type is a syntactic subsingleton.
+  That's to say, when each inductive type has at most one constructor.
+  Such types carry no data anyway.
+- Exception: if no inductive type has any constructors, these are likely stubbed-out declarations,
+  so we prefer `Type` instead.
+- Exception: if each constructor has no parameters, then these are likely partially-written enumerations,
+  so we prefer `Type` instead.
 -/
 private def isPropCandidate (numParams : Nat) (indTypes : List InductiveType) : MetaM Bool := do
   unless indTypes.foldl (fun n indType => max n indType.ctors.length) 0 == 1 do
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 73e9a588adb5..c77df6ff9ea5 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -633,8 +633,14 @@ where
         throwError msg
 
 /--
-Heuristic: we prefer a `Prop` instead of a `Type` structure when it could be a syntactic subsingleton.
-However, if there are no fields, we prefer `Type`.
+Decides whether the structure should be `Prop`-valued when the universe is not given
+and when the universe inference algorithm `collectUniversesFromFields` determines
+that the inductive type could naturally be `Prop`-valued.
+
+See `Lean.Elab.Command.isPropCandidate` for an explanation.
+Specialized to structures, the heuristic is that we prefer a `Prop` instead of a `Type` structure
+when it could be a syntactic subsingleton.
+Exception: no-field structures are `Type` since they are likely stubbed-out declarations.
 -/
 private def isPropCandidate (fieldInfos : Array StructFieldInfo) : Bool :=
   !fieldInfos.isEmpty