Skip to content

doc: fix incorrect examples of K-like reduction in RecursorVal docstring #13967

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
berberman wants to merge 2 commits into
base: master
Choose a base branch
from
Open

doc: fix incorrect examples of K-like reduction in RecursorVal docstring #13967

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
82b8d0d
doc: fix incorrect examples of K-like reduction in RecursorVal docstring
berberman Jun 7, 2026
62aee85
Update src/Lean/Declaration.lean
berberman Jun 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions src/Lean/Declaration.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading