From 82b8d0dd26463729e739b8a74b7b770d1f1c959e Mon Sep 17 00:00:00 2001 From: Potato Hatsue <1793913507@qq.com> Date: Sun, 7 Jun 2026 16:55:34 -0700 Subject: [PATCH 1/2] doc: fix incorrect examples of K-like reduction in RecursorVal docstring The previous docstring listed `Acc` and `And.intro` as examples of K-reduction. This is false because K-reduction strictly requires the single constructor to have 0 fields. Replace the incorrect examples. --- src/Lean/Declaration.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 3934023d7fce..0cb39ec0d585 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -369,12 +369,12 @@ 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 are `Exists` (which has a data field), `And` (which has two proof fields), + and `Or` (which has multiple constructors). -/ k : Bool isUnsafe : Bool From 62aee8500ccc5794461fd02e125ecbb2552c4823 Mon Sep 17 00:00:00 2001 From: Potato Hatsue Date: Wed, 10 Jun 2026 01:53:56 -0700 Subject: [PATCH 2/2] Update src/Lean/Declaration.lean Co-authored-by: Kyle Miller --- src/Lean/Declaration.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 0cb39ec0d585..52a32d4fdeae 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -373,8 +373,9 @@ structure RecursorVal extends ConstantVal where it has exactly one constructor, and that constructor has 0 fields. Examples of inductives with K-like reduction are `Eq`, `HEq`, and `True`. - Non-examples are `Exists` (which has a data field), `And` (which has two proof fields), - and `Or` (which has multiple constructors). + 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