Skip to content

feat: overriding binder kinds of parameters in inductive constructors#12603

Merged
kmill merged 2 commits intoleanprover:masterfrom
kmill:kmill_ind_ctor_binder
Feb 25, 2026
Merged

feat: overriding binder kinds of parameters in inductive constructors#12603
kmill merged 2 commits intoleanprover:masterfrom
kmill:kmill_ind_ctor_binder

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented Feb 20, 2026 •
edited
Loading

This PR adds a feature where inductive constructors can override the binder kinds of the type's parameters, like in #9480 for structure. For example, it's possible to make x explicit in the constructor Eq.refl, rather than implicit:

inductive Eq {α : Type u} (x : α) : α → Prop where
  | refl (x) : Eq x x

In the Prelude, this is currently accomplished by taking advantage of auto-promotion of indices to parameters.

Breaking change. Inductive types with a constructor that starts with typeless binders may need to be rewritten, e.g. changing (x) to (x : _) if there is a variable with that name or if it is meant to shadow one of the inductive type's parameters.

@kmill
feat: overriding binder kinds of parameters in inductive constructors
8aac484 
This PR adds a feature where `inductive` constructors can override the binder kinds of the type's parameters, like in leanprover#9480. For example, it's possible to make `x` explicit in the constructor `Eq.refl`:
```lean
inductive Eq {α : Type u} (x : α) : α → Prop where
  | refl (x) : Eq x x
```
@kmill kmill added the changelog-language Language features and metaprograms label Feb 20, 2026
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 20, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Feb 20, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-20 08:35:22)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 20, 2026
Update lean-toolchain for testing leanprover/lean4#12603
c72201d
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Feb 20, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 20, 2026
Update lean-toolchain for testing leanprover/lean4#12603
9e301ab
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Feb 20, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Feb 20, 2026

Mathlib CI status (docs):

@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Feb 20, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Feb 20, 2026

Mathlib CI status (docs):

@kmill kmill added this pull request to the merge queue Feb 25, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 25, 2026
@kmill kmill requested a review from TwoFX as a code owner February 25, 2026 02:09
@kmill kmill enabled auto-merge February 25, 2026 02:10
@kmill kmill added this pull request to the merge queue Feb 25, 2026
Merged via the queue into leanprover:master with commit de65af8 Feb 25, 2026
15 checks passed
kim-em added a commit to leanprover-community/aesop that referenced this pull request Feb 26, 2026
@kim-em
fix for leanprover/lean4#12603
eb17cd9
kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 1, 2026
@mathlib-nightly-testing @kim-em
@Ruben-VandeVelde @claude @joelriou @kmill @Kha @sgraf812
chore: adaptations for nightly-2026-02-25 (#192)
c19e7bb 
* revert changes to GCongr

* fix tests output again

* fix

* maxheartbeats

* fix

* chore: bump to nightly-2026-02-12

* merge lean-pr-testing-12412

* bump toolchain (early today, oops!)

* fix lakefile and lake update

* remove upstreamed

* restore a simp

* remove upstreamed and deprecation

* deprecation

* clarify adaptation note

* lake update

* fix for leanprover/lean4#11744

* fix indentation

* chore: bump to nightly-2026-02-13-rev1

* chore: bump to nightly-2026-02-13-rev2

* fix test

* fix test

* nice, most workarounds not needed with univ_out_params

* chore: bump to nightly-2026-02-14

* chore: update batteries for List.reverse_singleton fix

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* .

* add @[univ_out_params] where universe params are not determined by inputs

Classes like `Category.{v}`, `HasLimitsOfSize.{v₁,u₁}`, `Functor.IsContinuous.{t}`,
and `UCompactlyGeneratedSpace.{u}` have universe parameters that do not appear in
their input parameter types. With the new TC resolution cache (lean4#12286), these
default to output parameters, causing cache collisions when the same class is queried
at different universe levels.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* add #adaptation_note for @[univ_out_params] annotations

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* add library note on universe output parameters, update adaptation notes

Adds a library note in Category/Basic.lean explaining how `@[univ_out_params]`
interacts with the TC resolution cache, with concrete examples of when universe
parameters should and should not be treated as outputs.

Updates all adaptation notes to use a shorter form referencing this library note.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* convert #adaptation_note to -- comments for univ_out_params annotations

These are permanent annotations, not temporary workarounds, so
#adaptation_note is the wrong mechanism. Use regular comments placed
after the doc-string and before the @[univ_out_params] attribute.

Also restore the reference to lean4#12423 alongside lean4#12286.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* fix

* fix

* fix

* fix

* empty commit to retrigger CI

* chore: bump to nightly-2026-02-15

* lake update

* chore: bump to nightly-2026-02-15-rev1

* lake update

* chore: bump to nightly-2026-02-16

* Update lean-toolchain for leanprover/lean4#12179

* fix_backward_defeq script

* lake update batteries

* non-local set_option, added manually

* manual fixes, script confused by absence of blank lines

* times out without manual fix

* norm_num tests

* reduce_mod_char

* fix test output

* set_option globally in RingTheory.SimpleModule.Isotypic

* set_option globally in RingTheory.Adjoin.Dimension

* set_option a section of LinearAlgebra.FiniteDimensional.Basic

* set_option globally in Algebra.Homology.BifunctorAssociator

* set_option in section in Algebra.Homology.BifunctorHomotopy

* set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

* set_option globally in Algebra.Homology.BifunctorShift

* set_option in section in Geometry.Manifold.Riemannian.Basic

* set_option in section in NumberTheoryCyclotomic.Basic

* set_option in section in Analysis.Distribution.SchwartzSpace.Fourier

* global set_option in RingTheory.DedekindDomain.LinearDisjoint

* manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed

* manual fixes for CategoryTheory.Sites.Descent.IsStack

* manual fixes for Algebra.Homology.DifferentialObject

* manual fixes for Geometry.RingedSpace.PresheafedSpace

* manual fixes for CategoryTheory.Triangulated.Opposite.Functor

* manual fixes in Algebra.Homology.HomotopyCategory.ShortExact

* manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* manual fixes to CategoryTheory.Sites.Descent.DescentData

* manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string

* adaptation_note

* x: ./fix_backward_defeq.py

* x: ./fix_backward_defeq.py

* set_option linter.style.longFile

* remove unused simp args

* remove noop tactic

* lake update

* optimistic linter fixes

* patch and adaptation note

* slightly more care with the linter

* still getting it right

* fix test

* chore: adaptations for nightly-2026-02-15-rev1 (#177)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

* fix warning

* fix

* fix properly

* chore: adaptations for nightly-2026-02-16 (#179)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

* Merge master into nightly-testing

* chore: bump to nightly-2026-02-16-rev1

* move batteries back to nightly-testing

* lake update

* final fixes for leanprover/lean4#1279

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* chore: adaptations for nightly-2026-02-16-rev1 (#180)

* fix_backward_defeq script

* lake update batteries

* non-local set_option, added manually

* manual fixes, script confused by absence of blank lines

* times out without manual fix

* norm_num tests

* reduce_mod_char

* fix test output

* set_option globally in RingTheory.SimpleModule.Isotypic

* set_option globally in RingTheory.Adjoin.Dimension

* set_option a section of LinearAlgebra.FiniteDimensional.Basic

* set_option globally in Algebra.Homology.BifunctorAssociator

* set_option in section in Algebra.Homology.BifunctorHomotopy

* set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

* set_option globally in Algebra.Homology.BifunctorShift

* set_option in section in Geometry.Manifold.Riemannian.Basic

* set_option in section in NumberTheoryCyclotomic.Basic

* set_option in section in Analysis.Distribution.SchwartzSpace.Fourier

* global set_option in RingTheory.DedekindDomain.LinearDisjoint

* manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed

* manual fixes for CategoryTheory.Sites.Descent.IsStack

* manual fixes for Algebra.Homology.DifferentialObject

* manual fixes for Geometry.RingedSpace.PresheafedSpace

* manual fixes for CategoryTheory.Triangulated.Opposite.Functor

* manual fixes in Algebra.Homology.HomotopyCategory.ShortExact

* manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* manual fixes to CategoryTheory.Sites.Descent.DescentData

* manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string

* adaptation_note

* x: ./fix_backward_defeq.py

* x: ./fix_backward_defeq.py

* set_option linter.style.longFile

* remove unused simp args

* remove noop tactic

* lake update

* optimistic linter fixes

* patch and adaptation note

* slightly more care with the linter

* still getting it right

* fix test

* chore: adaptations for nightly-2026-02-16-rev1

* fix lakefile and manifest

* remove fix_backward_defeq.py

---------

Co-authored-by: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-17

* chore: remove fix_backward_defeq.py (no longer needed)

* Update lean-toolchain for testing leanprover/lean4#12538

* Update lean-toolchain for testing leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* temporary sorries to get further through the build

* fixes for sorries

* more set_option

* blech

* more fixes

* cleanup

* remove 316 set_options

* fix Algebra.Category.ModuleCat.Differentials.Presheaf

* remove unnecessary set_option

* remove more set_option backward.isDefEq.respectTransparency false

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-19

* chore: adaptations for nightly-2026-02-19

Rename instanceReducible to implicitReducible (lean4#12529).
Update batteries for upstreamed List.scanl/scanr (lean4#12452)
and Nat.Digits (lean4#12445).

* pre-emptively set toolchain

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* Update lean-toolchain for leanprover/lean4#12572

* remove set_option

* remove set_option

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12538

* remove more

* fixes for leanprover/lean4#12538

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* fixes for leanprover/lean4#12538

* fixes for leanprover/lean4#12538

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#12603

* chore: bump to nightly-2026-02-20

* fixes for leanprover/lean4#12538

* fixes

* Update lean-toolchain for testing leanprover/lean4#12625

* fix

* chore: adaptations for nightly-2026-02-20

* Merge master into nightly-testing

* fix

* chore: bump to nightly-2026-02-21

* chore: adaptations for nightly-2026-02-21

* Update lean-toolchain for leanprover/lean4#12625

* fix

* fixes

* fix

* Update lean-toolchain for leanprover/lean4#12538

* fixes

* fixes

* fixes

* chore: bump to nightly-2026-02-22

* fix cexample

* fix test

* Update lean-toolchain for leanprover/lean4#12625

* chore: adapt to mkHole type change from lean4#12459

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: adaptations for nightly-2026-02-22

* lake update

* bump batteries

* fixes

* Update lean-toolchain for leanprover/lean4#12564

* set_option

* set_option

* set_option

* fix(Linter/TextBased): don't flag "see adaptation note" comments

The `adaptationNoteLinter` was matching any line containing the
substring "daptation note", which caused false positives on lines
like `set_option maxHeartbeats 400000 in -- see adaptation note`
that merely reference a nearby `#adaptation_note` command.

Exclude lines containing `#adaptation_note` (correct usage) and
lines containing `see adaptation note` (cross-references).

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-23

* fixes

* adaptation notes

* fixes

* fixes

* fixes

* lint

* fix

* fix

* fix test

* fixes for leanprover/lean4#12650

* chore: adaptations for nightly-2026-02-23

* chore: bump to nightly-2026-02-23-rev1

* merge lean-pr-testing-12650

* chore: bump to nightly-2026-02-23-rev2

* x: scripts/add_set_option.py

* chore: bump to nightly-2026-02-25

* scripts/add_set_option.py

* fixes

* fixes

* fix

* fixes

* chore: bump to nightly-2026-02-25

* merge lean-pr-testing-12603

* bump batteries

* what happened there?

* lake update

* lake update aesop

* fixes

* chore: adaptations for nightly-2026-02-25

---------

Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: Claude Opus 4.6 <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Joël Riou <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Sebastian Graf <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kmill @leanprover-bot