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 : Std.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 CalcParams.instRpcEncodable : Lean.Server.RpcEncodable CalcParams

Equations

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

instance CalcParams.instFromJsonRpcEncodablePacket : Lean.FromJson CalcParams.RpcEncodablePacket✝

Equations

• CalcParams.instFromJsonRpcEncodablePacket = { fromJson? := CalcParams.fromJsonRpcEncodablePacket✝ }

instance CalcParams.instToJsonRpcEncodablePacket : Lean.ToJson CalcParams.RpcEncodablePacket✝

Equations

• CalcParams.instToJsonRpcEncodablePacket = { toJson := CalcParams.toJsonRpcEncodablePacket✝ }

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." "Calc 🔍"

def CalcPanel : ProofWidgets.Component CalcParams

The calc widget.

Equations

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