structure ProofWidgets.PanelWidgetProps : Type

In the infoview, an info block is a top-level collapsible block corresponding to a given location in a Lean file (e.g. with the header ▼ Basic.lean:12:34).

A panel widget is a component which can appear as a panel inside an info block in the infoview. For example, a tactic state display. The type PanelWidgetProps represents the props passed to a panel widget. The TypeScript version is exported as PanelWidgetProps from @leanprover/infoview.

Note that to be a good citizen which doesn't mess up the infoview layout, a panel widget should be a block element, and should provide some way to collapse it, for example by using <details> as the top-level tag.

• pos : Lean.Lsp.Position

  Cursor position in the file at which the widget is being displayed.

• goals : Array Lean.Widget.InteractiveGoal

  The current tactic-mode goals.

• termGoal? : Option Lean.Widget.InteractiveTermGoal

  The current term-mode goal, if any.

• selectedLocations : Array Lean.SubExpr.GoalsLocation

  Locations currently selected in the goal state.

instance ProofWidgets.instRpcEncodablePanelWidgetProps : Lean.Server.RpcEncodable ProofWidgets.PanelWidgetProps

Equations

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

def ProofWidgets.withPanelWidgetsTacticStx : Lean.ParserDescr

Display the selected panel widgets in the nested tactic script. For example, assuming we have written a GeometryDisplay component,

by with_panel_widgets [GeometryDisplay]
  simp
  rfl

will show the geometry display alongside the usual tactic state throughout the proof.

Equations

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

def ProofWidgets.withPanelWidgets : Lean.Elab.Tactic.Tactic

Equations

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