Skip to content

fix: ensure that tail-recursive List.flatten is used everywhere#12678

Merged
TwoFX merged 2 commits intoleanprover:masterfrom
TwoFX:flatten-noncomputable
Feb 25, 2026
Merged

fix: ensure that tail-recursive List.flatten is used everywhere#12678
TwoFX merged 2 commits intoleanprover:masterfrom
TwoFX:flatten-noncomputable

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Feb 24, 2026

This PR marks List.flatten, List.flatMap, List.intercalate as noncomputable to ensure that their csimp variants are used everywhere.

We also mark List.flatMapM as noncomputable and provide a tail-recursive implementation, and mark List.utf8Encode as noncomputable, which only exists for specification purposes anyway (at this point).

Closes #12676.

@TwoFX TwoFX requested a review from kim-em as a code owner February 24, 2026 18:34
@TwoFX TwoFX added the changelog-library Library label Feb 24, 2026
@TwoFX TwoFX enabled auto-merge February 24, 2026 18:35
@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 24, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

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

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-23-rev2 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-24 19:45:21)

@TwoFX TwoFX added this pull request to the merge queue Feb 25, 2026
Merged via the queue into leanprover:master with commit 87ec768 Feb 25, 2026
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

List.flatten is not tail recursive

2 participants