Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-28 20:09 8d3bd80b

View on Github →

feat(tactic/tidy): add tidy tactic (#285)

Estimated changes

Modified docs/tactics.md

Created tactic/auto_cases.lean

Modified tactic/basic.lean

Created tactic/chain.lean

added inductive tactic.tactic_script

Modified tactic/interactive.lean

Created tactic/tidy.lean

Modified tests/tactics.lean

Created tests/tidy.lean

added structure tidy.test.A

added structure tidy.test.B

added structure tidy.test.C

added structure tidy.test.D

added def tidy.test.d

added def tidy.test.f

added def tidy.test.tidy_test_0

added def tidy.test.tidy_test_1