mathlib documentation

tactic.tidy

source
meta def tactic.tidy.tidy_attribute  :
(user_attribute unit)

Tag interactive tactics (locally) with [tidy] to add them to the list of default tactics called by tidy.

source
meta def tactic.tidy.run_tactics  :
tactic string
source
meta def tactic.tidy.ext1_wrapper  :
tactic string
source
meta def tactic.tidy.default_tactics  :
list (tactic string)
source
meta structure tactic.tidy.cfg  :
Type
source
meta def tactic.tidy.core (cfg : tactic.tidy.cfg := {trace_result := ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) :
tactic (list string)
source
meta def tactic.tidy (cfg : tactic.tidy.cfg := {trace_result := ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) :
tactic unit
source
meta def tactic.interactive.tidy (trace : interactive.parse (lean.parser.tk "?")?) (cfg : tactic.tidy.cfg := {trace_result := 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.

source
meta def tactic.tidy_hole_cmd  :
hole_command

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.