def Lean.SubExpr.GoalsLocation.saveExprWithCtx (loc : Lean.SubExpr.GoalsLocation) : Lean.MetaM ProofWidgets.ExprWithCtx

Save the expression corresponding to a goals location.

Equations

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

structure ProofWidgets.GoalsLocationsToExprsParams : Type

• locations : Array (Lean.Server.WithRpcRef Lean.Elab.ContextInfo × Lean.SubExpr.GoalsLocation)

Instances For

• ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.instRpcEncodableGoalsLocationsToExprsParams

instance ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.toJsonRpcEncodablePacket✝ }

instance ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.instRpcEncodableGoalsLocationsToExprsParams : Lean.Server.RpcEncodable ProofWidgets.GoalsLocationsToExprsParams

Equations

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

instance ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.ProofWidgets.GoalsLocationsToExprsParams.fromJsonRpcEncodablePacket✝ }

structure ProofWidgets.GoalsLocationsToExprsResponse : Type

• exprs : Array (Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx)

Instances For

• ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.instRpcEncodableGoalsLocationsToExprsResponse

instance ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.instRpcEncodableGoalsLocationsToExprsResponse : Lean.Server.RpcEncodable ProofWidgets.GoalsLocationsToExprsResponse

Equations

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

instance ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.ProofWidgets.GoalsLocationsToExprsResponse.toJsonRpcEncodablePacket✝ }

def ProofWidgets.goalsLocationsToExprs (args : ProofWidgets.GoalsLocationsToExprsParams) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.GoalsLocationsToExprsResponse)

Compute expressions corresponding to the given GoalsLocations.

Equations

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

def ProofWidgets.SelectionPanel : ProofWidgets.Component ProofWidgets.PanelWidgetProps

Display a list of all expressions selected in the goal state, with a choice of which Expr presenter should be used to display each of those expressions.

Expressions can be selected using shift-click.

Equations

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