Commit 2022-10-17 23:07 f4484bd8

View on Github →

feat: port apply_rules from mathlib3 (#412)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/ApplyRules.lean

added def Mathlib.Tactic.applyRules

Created test/apply_rules.lean