Skip to content

fix: typo in application type mismatch error message#8290

Merged
TwoFX merged 3 commits intomasterfrom
markus/appplication
May 12, 2025
Merged

fix: typo in application type mismatch error message#8290
TwoFX merged 3 commits intomasterfrom
markus/appplication

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented May 12, 2025

This PR fixes a typo that was introduced recently.

@TwoFX TwoFX added the changelog-no Do not include this PR in the release changelog label May 12, 2025
@TwoFX TwoFX enabled auto-merge May 12, 2025 06:42
@TwoFX TwoFX disabled auto-merge May 12, 2025 06:56
@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 May 12, 2025
@ghost
Copy link
Copy Markdown

ghost commented May 12, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 10bda559f94b4b5bc39f1a0992cb70cb22cc7c26 --onto e681855428032555d8f1f45aebcbb0b4bad85db7. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-12 07:16:30)
  • ❌ Mathlib branch lean-pr-testing-8290 built against this PR, but testing failed. (2025-05-12 08:53:14) View Log
  • ✅ Mathlib branch lean-pr-testing-8290 has successfully built against this PR. (2025-05-12 09:10:38) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9105c01757db3d728e725469725fc0728ad8e718 --onto 2b4f372317f214e92988a79fc765586fbfb64e97. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-12 13:41:00)

@TwoFX TwoFX force-pushed the markus/appplication branch from a52fa5d to 0dd9ea9 Compare May 12, 2025 07:24
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 12, 2025
Update lean-toolchain for testing leanprover/lean4#8290
5436947
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025
Update lean-toolchain for testing leanprover/lean4#8290
4868cc0
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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 May 12, 2025
@TwoFX TwoFX added this pull request to the merge queue May 12, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks May 12, 2025
@TwoFX TwoFX enabled auto-merge May 12, 2025 13:18
@TwoFX TwoFX added this pull request to the merge queue May 12, 2025
Merged via the queue into master with commit eda467e May 12, 2025
16 checks passed
@TwoFX TwoFX deleted the markus/appplication branch August 4, 2025 07:19
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

builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog 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

@TwoFX