Documentation

ProofWidgets.Component.Basic

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

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.

Instances For
    Equations
    • ProofWidgets.instToModuleComponent = { toModule := ProofWidgets.Component.toModule }

    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.
    Instances For

      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.
      Instances For

        Present a structured Lean message.

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