Skip to content

fix: arg conv tactic misreported number of arguments on error#5968

Merged
kmill merged 2 commits intoleanprover:masterfrom
kmill:fix_conv_arg_error_msg
Nov 6, 2024
Merged

fix: arg conv tactic misreported number of arguments on error#5968
kmill merged 2 commits intoleanprover:masterfrom
kmill:fix_conv_arg_error_msg

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented Nov 5, 2024

No description provided.

@kmill kmill requested a review from kim-em as a code owner November 5, 2024 20:27
@kmill kmill enabled auto-merge November 5, 2024 20:33
@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 Nov 5, 2024
@ghost
Copy link
Copy Markdown

ghost commented Nov 5, 2024 •
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 c157ddda11c052c6bf061a2cec38a72b17de2661 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-05 20:53:41)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5d2bd1e2e4ab4212f347c08cd7464b673f9e1c39 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 02:07:34)

@kmill kmill force-pushed the fix_conv_arg_error_msg branch from 40291d6 to 3edd701 Compare November 6, 2024 01:50
@kmill kmill added this pull request to the merge queue Nov 6, 2024
Merged via the queue into leanprover:master with commit 406da78 Nov 6, 2024
@kim-em kim-em added the changelog-language Language features and metaprograms label Jan 4, 2025
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@kmill @JovanGerb
fix: arg conv tactic misreported number of arguments on error (lean…
54297a7 
…prover#5968)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms 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 @kim-em