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

chore: add public modifiers in Lean.Elab.Tactic.Induction (#10810)

Browse source
This commit is contained in:
Kim Morrison 2025-10-17 08:52:02 +11:00 • committed by GitHub
parent 127fe785a3
commit effde06296
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -856,7 +856,9 @@ Returns
Modifies the current goal when generalizing.
-/
def elabElimTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId)) :=
-- This is public for now as it is used in Mathlib's `induction'` and `cases'` tactics,
-- which are no longer used in Mathlib, but are still prevalent in downstream projects.
public def elabElimTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId)) :=
withMainContext do
let infos : Array ElimTargetInfo ← targets.mapM fun target => do
let view ← mkTargetView target
@ -910,7 +912,9 @@ def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
result := result.push expr
return (result, [mvarId])
def checkInductionTargets (targets : Array Expr) : MetaM Unit := do
-- This is public for now as it is used in Mathlib's `induction'` tactic,
-- which is no longer used in Mathlib, but still prevalent in downstream projects.
public def checkInductionTargets (targets : Array Expr) : MetaM Unit := do
let mut foundFVars : FVarIdSet := {}
for target in targets do
unless target.isFVar do