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 (ProofWidgets.Component Props)

Equations

• ProofWidgets.instToModuleComponent = { toModule := ProofWidgets.Component.toModule }

structure ProofWidgets.InteractiveCodeProps : Type

• fmt : Lean.Widget.CodeWithInfos

instance ProofWidgets.instRpcEncodableInteractiveCodeProps : Lean.Server.RpcEncodable ProofWidgets.InteractiveCodeProps

Equations

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

def ProofWidgets.InteractiveCode : ProofWidgets.Component ProofWidgets.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.

Equations

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

structure ProofWidgets.InteractiveExprProps : Type

• expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx

instance ProofWidgets.instRpcEncodableInteractiveExprProps : Lean.Server.RpcEncodable ProofWidgets.InteractiveExprProps

Equations

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

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

Equations

• ProofWidgets.ppExprTagged { expr := { val := expr } } = Lean.Server.RequestM.asTask (liftM (expr.runMetaM fun (e : Lean.Expr) => Lean.Widget.ppExprTagged e))

def ProofWidgets.InteractiveExpr : ProofWidgets.Component ProofWidgets.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.

Equations

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

structure ProofWidgets.InteractiveMessageProps : Type

• msg : Lean.Server.WithRpcRef Lean.MessageData

instance ProofWidgets.instRpcEncodableInteractiveMessageProps : Lean.Server.RpcEncodable ProofWidgets.InteractiveMessageProps

Equations

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

def ProofWidgets.InteractiveMessage : ProofWidgets.Component ProofWidgets.InteractiveMessageProps

Present a structured Lean message.

Equations

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

structure ProofWidgets.MarkdownDisplay.Props : Type

• contents : String

instance ProofWidgets.MarkdownDisplay.instToJsonProps : Lean.ToJson ProofWidgets.MarkdownDisplay.Props

Equations

• ProofWidgets.MarkdownDisplay.instToJsonProps = { toJson := ProofWidgets.MarkdownDisplay.toJsonProps✝ }

instance ProofWidgets.MarkdownDisplay.instFromJsonProps : Lean.FromJson ProofWidgets.MarkdownDisplay.Props

Equations

• ProofWidgets.MarkdownDisplay.instFromJsonProps = { fromJson? := ProofWidgets.MarkdownDisplay.fromJsonProps✝ }

def ProofWidgets.MarkdownDisplay : ProofWidgets.Component ProofWidgets.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$"} />

Equations

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

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

Construct a structured message from a ProofWidgets component.

For the meaning of alt, see MessageData.ofWidget.

Equations

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