mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

feat: propagate_tags tactic

Open Beanway144 opened this issue 2 years ago • 1 comments

Adds propagate_tags

Beanway144 avatar Apr 05 '22 00:04 Beanway144

@Beanway144, sorry this languished on the PR queue for a while. Would you be able to merge the conflict and adopt Mario's suggestions?

kim-em avatar Jul 27 '22 02:07 kim-em