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

fix: spurious warning message in grind (#10962)

Browse source 
This PR fixes a spurious warning message in `grind`.

Closes #10670
This commit is contained in:
Leonardo de Moura 2025-10-25 19:40:12 -07:00 • committed by GitHub
parent 2f3211028b
commit feb864712f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 17 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Elab/Tactic/Grind/Main.lean
View file

@ -185,7 +185,8 @@ where
-- If it is an inductive predicate,
-- we also add the constructors (intro rules) as E-matching rules
for ctor in info.ctors do
params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
-- **Note**: We should not warn if `declName` is an inductive
params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
else
params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
| .symbol prio =>
@ -195,7 +196,7 @@ where
addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
(kind : Grind.EMatchTheoremKind)
(minIndexable : Bool) (suggest : Bool := false) : MetaM Grind.Params := do
(minIndexable : Bool) (suggest : Bool := false) (warn := true) : MetaM Grind.Params := do
let info ← getAsyncConstInfo declName
match info.kind with
| .thm | .axiom | .ctor =>
@ -204,7 +205,8 @@ where
ensureNoMinIndexable minIndexable
let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
if params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
if warn &&
params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
warnRedundantEMatchArg params.ematch declName
return { params with extra := params.extra.push thm₁ |>.push thm₂ }
@ -215,7 +217,7 @@ where
Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
else
Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then
warnRedundantEMatchArg params.ematch declName
return { params with extra := params.extra.push thm }
| .defn =>

11
tests/lean/run/grind_10670.lean Normal file
View file

@ -0,0 +1,11 @@
inductive Foo : Nat → Prop
| one : Foo 1
| two : Foo 2
attribute [grind ·] Foo.one
#guard_msgs in
example {l : Nat} (hl : Foo l) : Foo (3 - l) := by
induction hl with
| one => grind [Foo]
| two => grind