Documentation

Mathlib.Tactic.Widget.Conv

Conv widget #

This is a slightly improved version of one of the examples in the ProofWidget library. It defines a conv? tactic that displays a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal.

source
def insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Lean.Expr) (params : SelectInsertParams) :
Lean.MetaM (String × String × Option (String.Pos × String.Pos))

Return the link text and inserted text above and below of the conv widget.

Equations
    Instances For
      source
      def ConvSelectionPanel.rpc (params : SelectInsertParams) :
      Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

      Rpc function for the conv widget.

      Equations
        Instances For
          source
          def ConvSelectionPanel :
          ProofWidgets.Component SelectInsertParams

          The conv widget.

          Equations
            Instances For
              source
              def tacticConv? :
              Lean.ParserDescr

              Display a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal.

              Equations
                Instances For