Documentation

Mathlib.Tactic.Widget.Calc

Calc widget #

This file redefines the calc tactic so that it displays a widget panel allowing to create new calc steps with holes specified by selected sub-expressions in the goal.

source
def createCalc :
Batteries.CodeAction.TacticCodeAction

Code action to create a calc tactic from the current goal.

Equations
    Instances For
      source
      structure CalcParamsextends SelectInsertParams :
      Type

      Parameters for the calc widget.

      Instances For
        source
        instance instSelectInsertParamsClassCalcParams :
        SelectInsertParamsClass CalcParams
        Equations
          source
          instance instRpcEncodableCalcParams :
          Lean.Server.RpcEncodable CalcParams
          Equations
            source
            def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Lean.Expr) (params : CalcParams) :
            Lean.MetaM (String × String × Option (String.Pos × String.Pos))

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

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

                Rpc function for the calc widget.

                Equations
                  Instances For
                    source
                    def CalcPanel :
                    ProofWidgets.Component CalcParams

                    The calc widget.

                    Equations
                      Instances For
                        source
                        def Lean.Elab.Tactic.tacticCalc? :
                        ParserDescr

                        Create a calc proof.

                        Equations
                          Instances For