Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-10 14:01 d6f84dae

View on Github →

feat(tactic/tidy): add tidy? syntax for reporting a tactic script (#704)

Estimated changes

Modified docs/tactics.md

Modified src/tactic/tidy.lean

Modified test/tidy.lean

modified structure tidy.test.B

modified def tidy.test.d

modified def tidy.test.tidy_test_0

modified def tidy.test.tidy_test_1