Skip to content

chore: List/Array/Vector implicitness changes#7739

Merged
kim-em merged 1 commit intomasterfrom
implicitness2
Mar 30, 2025
Merged

chore: List/Array/Vector implicitness changes#7739
kim-em merged 1 commit intomasterfrom
implicitness2

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Mar 30, 2025

This PR makes some changes to implicitness of arguments based on review of changes in Mathlib following from #7672.

@kim-em kim-em enabled auto-merge March 30, 2025 22:34
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 30, 2025 22:47 Inactive
@kim-em kim-em added this pull request to the merge queue Mar 30, 2025
@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 Mar 30, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 30, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d0d31e509f5c7f08f21738e1f94f1b518138580f --onto 12a21e79c71880424321d62e60449863c504048a. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-30 23:09:17)

Merged via the queue into master with commit 866c807 Mar 30, 2025
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

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.

1 participant

@kim-em