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.

def createCalc : Batteries.CodeAction.TacticCodeAction

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

Equations

• One or more equations did not get rendered due to their size.
• createCalc _params _snap ctx _stack node = pure #[]

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 : Nat

  indentation level of the calc block.

instance instSelectInsertParamsClassCalcParams : SelectInsertParamsClass CalcParams

Equations

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

instance instRpcEncodableCalcParams : Lean.Server.RpcEncodable CalcParams

Equations

• instRpcEncodableCalcParams = { rpcEncode := instRpcEncodableCalcParams.enc✝, rpcDecode := instRpcEncodableCalcParams.dec✝ }

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

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

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

Rpc function for the calc widget.

Equations

• CalcPanel.rpc = mkSelectionPanelRPC suggestSteps "Please select subterms using Shift-click." "Calc 🔍"

def CalcPanel : ProofWidgets.Component CalcParams

The calc widget.

Equations

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

def Lean.Elab.Tactic.tacticCalc? : ParserDescr

Create a calc proof.

Equations

• Lean.Elab.Tactic.tacticCalc? = Lean.ParserDescr.node `Lean.Elab.Tactic.tacticCalc? 1024 (Lean.ParserDescr.nonReservedSymbol "calc?" false)