(tactic/tidy): add docstring [skip ci] (#1788)

* (tactic/tidy): add docstring [skip ci]

* Update src/tactic/tidy.lean

* mention [tidy] attribute

src/tactic/tidy.lean

@@ -79,6 +79,15 @@ meta def tidy (cfg : tidy.cfg := {}) := tactic.tidy.core cfg >> skip
 namespace interactive
 open lean.parser interactive
 
+/-- Use a variety of conservative tactics to solve goals.
+`tidy?` reports back the tactic script it found.
+The default list of tactics is stored in `tactic.tidy.default_tidy_tactics`.
+This list can be overridden using `tidy { tactics := ... }`.
+(The list must be a `list` of `tactic string`, so that `tidy?`
+can report a usable tactic script.) 
+
+Tactics can also be added to the list by tagging them (locally) with the
+`[tidy]` attribute. -/
 meta def tidy (trace : parse $ optional (tk "?")) (cfg : tidy.cfg := {}) :=
 tactic.tidy { trace_result := trace.is_some, ..cfg }
 end interactive