Tag interactive tactics (locally) with [tidy] to add them to the list of default tactics
called by tidy.
def
tactic.tidy.core
:
(tactic.tidy.cfg := {trace_result := bool.ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) → tactic (list string)
def
tactic.tidy
:
(tactic.tidy.cfg := {trace_result := bool.ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) → tactic unit
def
tactic.interactive.tidy
:
interactive.parse (optional (lean.parser.tk "?")) → (tactic.tidy.cfg := {trace_result := bool.ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) → tactic unit
Use a variety of conservative tactics to solve goals.
tidy? reports back the tactic script it found. As an example
example : ∀ x : unit, x = unit.star :=
begin
tidy? -- Prints the trace message: "Try this: intros x, exact dec_trivial"
end
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.
Invoking the hole command tidy ("Use tidy to complete the goal") runs the tactic of
the same name, replacing the hole with the tactic script tidy produces.