10000 chore: rename (co)inductive predicates keyword and the names of their associated fixpoint (co)induction principles by wkrozowski · Pull Request #8948 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

chore: rename (co)inductive predicates keyword and the names of their associated fixpoint (co)induction principles #8948

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

Jump to bottom
Merged
merged 3 commits into from
Jun 23, 2025
Merged

chore: rename (co)inductive predicates keyword and the names of their associated fixpoint (co)induction principles #8948

merged 3 commits into from
Jun 23, 2025

Conversation

wkrozowski
Copy link
Contributor

This PR renames greatest_fixpoint to coinductive_fixpoint and least_fixpoint to inductive_fixpoint for improved clarity and consistency.

Additionally, the associated fixpoint induction principles previously named fixpoint_induct are now renamed to coinduct or induct, depending on whether they correspond to a coinductive_fixpoint or an inductive_fixpoint.

To maintain consistency across the codebase, all relevant references in the standard library that use (co)inductive predicates have been updated to follow the new naming convention.

@wkrozowski wkrozowski requested a review from nomeata June 23, 2025 15:44
@wkrozowski wkrozowski requested a review from TwoFX as a code owner June 23, 2025 15:44
@wkrozowski wkrozowski added merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. changelog-language Language features, tactics, and metaprograms changelog-library Library labels Jun 23, 2025
@wkrozowski wkrozowski mentioned this pull request Jun 23, 2025
Closed
@wkrozowski wkrozowski force-pushed the wojciech/coinduction_name_change2 branch from b22daba to cb5edc8 Compare June 23, 2025 16:15
@wkrozowski wkrozowski requested a review from tydeu as a code owner June 23, 2025 16:21
@wkrozowski wkrozowski marked this pull request as draft June 23, 2025 16:29
@wkrozowski wkrozowski force-pushed the wojciech/coinduction_name_change2 branch from f1d5fb2 to cb5edc8 Compare June 23, 2025 16:35
@wkrozowski wkrozowski removed request for tydeu and TwoFX June 23, 2025 16:36
@wkrozowski wkrozowski force-pushed the wojciech/coinduction_name_change2 branch 2 times, most recently from c1b6f3d to cb5edc8 Compare June 23, 2025 17:17
@wkrozowski
chore: rename keywords for (co)inductive predicates and the names of …
8a86edb 
…their associated (co)induction principle
8000
s

chore: rename `fixpoint_induct` to `induct` and `coinduct` for (co)inductive predicates
@wkrozowski
chore: update stage0
230cdc8
@wkrozowski
chore: rename keywords for (co)inductive predicates and the names of …
e4764a5 
…the associated (co)induction principles
@wkrozowski wkrozowski force-pushed the wojciech/coinduction_name_change2 branch from cb5edc8 to e4764a5 Compare June 23, 2025 17:38
@wkrozowski wkrozowski marked this pull request as ready for review June 23, 2025 17:50
@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 Jun 23, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ecf670e08c62a38a90be022d583b3aa462506805 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-23 18:05:46)

@nomeata nomeata merged commit 22cd34c into leanprover:master Jun 23, 2025
16 checks passed
@wkrozowski wkrozowski deleted the wojciech/coinduction_name_change2 branch June 23, 2025 18:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nomeata nomeata nomeata approved these changes

Assignees
No one assigned
Labels
changelog-language Language features, tactics, and metaprograms changelog-library Library merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. 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.
3 participants
@wkrozowski @leanprover-community-bot @nomeata
0