Documentation

Mathlib.Tactic.Hint

The hint tactic. #

The hint tactic tries the kitchen sink: it runs every tactic registered via the register_hint tac command on the current goal, and reports which ones succeed.

Future work #

It would be nice to run the tactics in parallel.

An environment extension for registering hint tactics.

Register a new hint tactic.

Equations
    Instances For

      Return the list of registered hint tactics.

      Equations
        Instances For

          Register a tactic for use with the hint tactic, e.g. register_hint simp_all.

          Equations
            Instances For

              Construct a suggestion for a tactic.

              • Check the passed MessageLog for an info message beginning with "Try this: ".
              • If found, use that as the suggestion.
              • Otherwise use the provided syntax.
              • Also, look for remaining goals and pretty print them after the suggestion.
              Equations
                Instances For

                  Run a tactic, returning any new messages rather than adding them to the message log.

                  Equations
                    Instances For

                      Run a tactic, but revert any changes to info trees. We use this to inhibit the creation of widgets by subsidiary tactics.

                      Equations
                        Instances For

                          Run all tactics registered using register_hint. Print a "Try these:" suggestion for each of the successful tactics.

                          If one tactic succeeds and closes the goal, we don't look at subsequent tactics.

                          Equations
                            Instances For

                              The hint tactic tries every tactic registered using register_hint tac, and reports any that succeed.

                              Equations
                                Instances For