mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: substs tactic

Open evanlohn opened this issue 3 years ago • 3 comments
trafficstars

Added the substs tactic, which just applies subst to multiple hypotheses at once.

This is my first PR to mathlib; let me know what needs to change!

evanlohn avatar Jul 18 '22 20:07 evanlohn

you need to add import Mathlib.Tactic.Substs to Mathlib.lean

digama0 avatar Jul 19 '22 03:07 digama0

bors r+

digama0 avatar Jul 19 '22 21:07 digama0

Build failed:

bors[bot] avatar Jul 19 '22 21:07 bors[bot]

bors r+

gebner avatar Aug 24 '22 14:08 gebner

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 24 '22 14:08 bors[bot]

Thanks!

Please remove the "awaiting-author" label in the future when you've applied the changes from code review.

gebner avatar Aug 24 '22 14:08 gebner