structure ProofWidgets.Component (Props : Type) extends Lean.Widget.Module : Type

A component is a widget module with a default or named export which is a React component. Every component definition must be annotated with @[widget_module]. This makes it possible for the infoview to load the component.

Execution environment

The JS environment in which components execute provides a fixed set of libraries accessible via direct import, notably @leanprover/infoview. All React contexts exported from @leanprover/infoview are usable from components.

Lean encoding of props

Props is the Lean representation of the type JsProps of React props that the component expects. The export of the module specified in «export» should then have type (props: JsProps & { pos: DocumentPosition }): React.ReactNode where DocumentPosition is defined in @leanprover/infoview. Props is expected to have a Lean.Server.RpcEncodable instance specifying how to encode props as JSON.

Note that by defining a Component Props with a specific JS implementation, you are asserting that Props is a correct representation of JsProps.

• javascript : String
• javascriptHash : { x : UInt64 // x = hash self.javascript }
• export : String

  Which export of the module to use as the component function.

instance ProofWidgets.instToModuleComponent {Props : Type} : Lean.Widget.ToModule (Component Props)

structure ProofWidgets.InteractiveCodeProps : Type

• fmt : Lean.Widget.CodeWithInfos

instance ProofWidgets.instRpcEncodableInteractiveCodeProps : Lean.Server.RpcEncodable InteractiveCodeProps

def ProofWidgets.InteractiveCode : Component InteractiveCodeProps

Present pretty-printed code as interactive text.

The most common use case is to instantiate this component from a Lean.Expr. To do so, you must eagerly pretty-print the Expr using Widget.ppExprTagged. See also InteractiveExpr.

structure ProofWidgets.InteractiveExprProps : Type

• expr : Lean.Server.WithRpcRef ExprWithCtx

instance ProofWidgets.instRpcEncodableInteractiveExprProps : Lean.Server.RpcEncodable InteractiveExprProps

def ProofWidgets.ppExprTagged : InteractiveExprProps → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Widget.CodeWithInfos)

def ProofWidgets.InteractiveExpr : Component InteractiveExprProps

Lazily pretty-print and present a Lean.Expr as interactive text.

This component is preferrable over InteractiveCode when the Expr will not necessarily be displayed in the UI (e.g. it may be hidden by default), in which case laziness saves some work. On the other hand if the Expr will likely be shown and you are in a MetaM context, it is preferrable to use the eager InteractiveCode in order to avoid the extra client-server roundtrip needed for the pretty-printing RPC call.

structure ProofWidgets.InteractiveMessageProps : Type

• msg : Lean.Server.WithRpcRef Lean.MessageData

instance ProofWidgets.instRpcEncodableInteractiveMessageProps : Lean.Server.RpcEncodable InteractiveMessageProps

def ProofWidgets.InteractiveMessage : Component InteractiveMessageProps

Present a structured Lean message.

structure ProofWidgets.MarkdownDisplay.Props : Type

• contents : String

instance ProofWidgets.MarkdownDisplay.instToJsonProps : Lean.ToJson Props

instance ProofWidgets.MarkdownDisplay.instFromJsonProps : Lean.FromJson Props

def ProofWidgets.MarkdownDisplay : Component MarkdownDisplay.Props

Render a given string as Markdown. LaTeX is supported with MathJax: use $...$ for inline math, and $$...$$ for displayed math.

Example usage:

<MarkdownDisplay contents={"$a + b = c$"} />

def Lean.MessageData.ofComponent {Props : Type} [Server.RpcEncodable Props] (c : ProofWidgets.Component Props) (p : Props) (alt : String) : CoreM MessageData

Construct a structured message from a ProofWidgets component.

For the meaning of alt, see MessageData.ofWidget.