diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 3934023d7fce..52a32d4fdeae 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -369,12 +369,13 @@ structure RecursorVal extends ConstantVal where
   rules : List RecursorRule
   /-- It supports K-like reduction.
   A recursor is said to support K-like reduction if one can assume it behaves
-  like `Eq` under axiom `K` --- that is, it has one constructor, the constructor has 0 arguments,
-  and it is an inductive predicate (ie, it lives in Prop).
+  like `Eq` under axiom `K` --- that is, it is an inductive predicate (i.e., it lives in `Prop`),
+  it has exactly one constructor, and that constructor has 0 fields.
 
-  Examples of inductives with K-like reduction is `Eq`, `Acc`, and `And.intro`.
-  Non-examples are `exists` (where the constructor has arguments) and
-    `Or.intro` (which has multiple constructors).
+  Examples of inductives with K-like reduction are `Eq`, `HEq`, and `True`.
+  Non-examples include those with multiple constructors (like `Or`)
+  and those whose constructor has one or more fields (like `And`, `Exists`,
+  and `Nonempty').
   -/
   k : Bool
   isUnsafe : Bool