Commit 2022-05-03 10:16 f2a316c0

View on Github →

feat: left and right tactics (#260) left and right tactics implemented with tests/examples

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/LeftRight.lean

added def Mathlib.Tactic.LeftRight.leftRightMeta

Created test/left_right.lean

added def two:

added def zero: