mathlib3 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
def tactic_doc.attribute.tidy  :
tactic_doc_entry

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 := bool.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 := bool.ff, trace_result_prefix := "Try this: ", tactics := tactic.tidy.default_tactics}) :
tactic unit
source
meta def tactic.interactive.tidy (trace : interactive.parse (optional (lean.parser.tk "?"))) (cfg : 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.

source
def tactic_doc.tactic.tidy  :
tactic_doc_entry

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.

source
def tactic_doc.hole_command.tidy  :
tactic_doc_entry

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.