mathlib documentation

tactic.tidy

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

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

meta structure tactic.tidy.cfg  :
Type

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.

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.

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.