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
🔸 coverage
def createCalc :
Batteries.CodeAction.TacticCodeAction

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

Instances For
    source
    🔶 coverage
    structure CalcParamsextends SelectInsertParams :
    Type

    Parameters for the calc widget.

    • pos : Lean.Lsp.Position
    • goals : Array Lean.Widget.InteractiveGoal
    • selectedLocations : Array Lean.SubExpr.GoalsLocation
    • replaceRange : Lean.Lsp.Range
    • isFirst : Bool

      Is this the first calc step?

    • indent : â„•

      indentation level of the calc block.

    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance instSelectInsertParamsClassCalcParams :
      SelectInsertParamsClass CalcParams
      source
      🔸 coverage
      @[implicit_reducible]
      instance instRpcEncodableCalcParams :
      Lean.Server.RpcEncodable CalcParams
      source
      🔸 coverage
      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
        🔸 coverage
        def CalcPanel.rpc (params : CalcParams) :
        Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

        Rpc function for the calc widget.

        Instances For
          source
          🔸 coverage
          def CalcPanel :
          ProofWidgets.Component CalcParams

          The calc widget.

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

            Create a calc proof.

            Instances For