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)

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

Equations

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

structure ProofWidgets.GoalsLocationsToExprsResponse : Type

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

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

Equations

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

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.