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.

Instances For
    source
    structure CalcParams extends SelectInsertParams :
    Type

    Parameters for the calc widget.

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

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

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

        Rpc function for the calc widget.

        Instances For
          source
          def CalcPanel :
          ProofWidgets.Component CalcParams

          The calc widget.

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

            Create a calc proof.

            Instances For