Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Oct 20, 2025

This PR fixes an issue where adding a missing case name after the pipe in induction would not remove the now-obsolete error message.

Fixes #10847

@Kha Kha requested a review from kim-em as a code owner October 20, 2025 07:46
@Kha Kha enabled auto-merge October 20, 2025 07:47
@nomeata
Copy link
Collaborator

nomeata commented Oct 20, 2025

Does this fix #10847?

@Kha Kha added the changelog-tactics User facing tactics label Oct 20, 2025
@Kha Kha added this pull request to the merge queue Oct 20, 2025
Merged via the queue into leanprover:master with commit 0d5869b Oct 20, 2025
20 of 21 checks passed
@Kha Kha deleted the push-uoxssqmlpopp branch October 20, 2025 09:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

spacing bug with induction tactic

2 participants