Documentation

Mathlib.Tactic.Widget.SelectPanelUtils

Selection panel utilities #

The main declaration is mkSelectionPanelRPC which helps creating rpc methods for widgets generating tactic calls based on selected sub-expressions in the main goal.

There are also some minor helper functions.

Given a Array GoalsLocation return the array of SubExpr.Pos for all locations in the targets of the relevant goals.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Replace the sub-expression at the given position by a fresh meta-variable.

    Equations
    Instances For

      Replace all meta-variable names by "?_".

      Equations
      • s.renameMetaVar = match s.splitOn "?m." with | [] => "" | [s] => s | head :: tail => head ++ "?_" ++ "?_".intercalate (List.map (fun (s : String) => s.dropWhile Char.isDigit) tail)
      Instances For

        Structures providing parameters for a Select and insert widget.

        Instances For
          Equations
          • One or more equations did not get rendered due to their size.

          Helper function to create a widget allowing to select parts of the main goal and then display a link that will insert some tactic call.

          The main argument is mkCmdStr which is a function creating the link text and the tactic call text. The helpMsg argument is displayed when nothing is selected and title is used as a panel title. The onlyGoal argument says whether the selected has to be in the goal. Otherwise it can be in the local context. The onlyOne argument says whether one should select only one sub-expression. In every cases, all selected subexpressions should be in the main goal or its local context.

          The last arguments params should not be provided so that the output has type Params → RequestM (RequestTask Html) and can be fed to the mk_rpc_widget% elaborator.

          Note that the pos and goalType arguments to mkCmdStr could be extracted for the Params argument but that extraction would happen in every example, hence it is factored out here. We also make sure mkCmdStr is executed in the right context.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For