Def Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly

Modification history

2025-11-09 19:24

Mathlib/Tactic/GeneralizeProofs.lean

chore: adaptations for batteries#1496 (#31437)

Deleted Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly View on Github →

2024-04-29 01:28

Mathlib/Tactic/GeneralizeProofs.lean

feat: make `generalize_proofs` handle proofs under binders (#12472) …

Added Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly View on Github →