max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: missing word in inductionWithNoAlts error message (#11684)

Browse source 
This PR adds a missing word ("be") to the error message catching
natural-numbers-game-like uses of induction that was introduced in
#11347.
This commit is contained in:
Robert J. Simmons 2025-12-15 12:23:25 -05:00 • committed by GitHub
parent 949cf69246
commit 7b8e51e025
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Induction.lean
View file

@ -665,7 +665,7 @@ def checkForInductionWithNoAlts (tacticKind : String) (optInductionAlts : Syntax
-- Usually errors are suppressed for syntax containing `.missing` nodes, but this named error is
-- listed in `Lean.Core.getAndEmptySnapshotTasks` as an error that ignores suppression.
throwNamedErrorAt optInductionAlts lean.inductionWithNoAlts
m!"Invalid syntax for {tacticKind} tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `{var}`."
m!"Invalid syntax for {tacticKind} tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `{var}`."
/--
Separate out the optional `with` tactics from the rest of the alternates

4
tests/lean/notNaturalNumbersGame.lean.expected.out
View file

@ -1,7 +1,7 @@
notNaturalNumbersGame.lean:6:20: error: unknown tactic
notNaturalNumbersGame.lean:6:14-6:20: error(lean.inductionWithNoAlts): Invalid syntax for induction tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
notNaturalNumbersGame.lean:6:14-6:20: error(lean.inductionWithNoAlts): Invalid syntax for induction tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
notNaturalNumbersGame.lean:13:16: error: unknown tactic
notNaturalNumbersGame.lean:13:10-13:16: error(lean.inductionWithNoAlts): Invalid syntax for case analysis tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
notNaturalNumbersGame.lean:13:10-13:16: error(lean.inductionWithNoAlts): Invalid syntax for case analysis tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
notNaturalNumbersGame.lean:22:2-22:11: error: Alternative `zero` has not been provided
notNaturalNumbersGame.lean:22:2-22:11: error: Alternative `succ` has not been provided
notNaturalNumbersGame.lean:25:2-25:7: error: Alternative `zero` has not been provided