structure Lean.Widget.WidgetInstance : Type

An instance of a widget component: the identifier of a widget module and the hash of its JS source code together with props.

See the manual entry for more information about widgets.

• id : Lake.Name

  Name of the @[widget_module].

• javascriptHash : UInt64

  Hash of the JS source of the widget module.

• props : StateM Lean.Server.RpcObjectStore Lean.Json

  Arguments to be passed to the component's default exported function.

  Props may contain RPC references, so must be stored as a computation with access to the RPC object store.

instance Lean.Widget.Lean.Widget.WidgetInstance.instFromJsonRpcEncodablePacket : Lean.FromJson Lean.Widget.Lean.Widget.WidgetInstance.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.WidgetInstance.instFromJsonRpcEncodablePacket = { fromJson? := Lean.Widget.Lean.Widget.WidgetInstance.fromJsonRpcEncodablePacket✝ }

instance Lean.Widget.Lean.Widget.WidgetInstance.instRpcEncodableWidgetInstance : Lean.Server.RpcEncodable Lean.Widget.WidgetInstance

Equations

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

instance Lean.Widget.Lean.Widget.WidgetInstance.instToJsonRpcEncodablePacket : Lean.ToJson Lean.Widget.Lean.Widget.WidgetInstance.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.WidgetInstance.instToJsonRpcEncodablePacket = { toJson := Lean.Widget.Lean.Widget.WidgetInstance.toJsonRpcEncodablePacket✝ }