structure ProofWidgets.PenroseDiagramProps : Type

• embeds : Array (String × ProofWidgets.Html)
• dsl : String
• sty : String
• sub : String

instance ProofWidgets.instInhabitedPenroseDiagramProps : Inhabited ProofWidgets.PenroseDiagramProps

Equations

• ProofWidgets.instInhabitedPenroseDiagramProps = { default := { embeds := default, dsl := default, sty := default, sub := default } }

instance ProofWidgets.PenroseDiagramProps.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.PenroseDiagramProps.RpcEncodablePacket✝

Equations

• ProofWidgets.PenroseDiagramProps.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.PenroseDiagramProps.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.PenroseDiagramProps.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.PenroseDiagramProps.RpcEncodablePacket✝

Equations

• ProofWidgets.PenroseDiagramProps.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.PenroseDiagramProps.toJsonRpcEncodablePacket✝ }

instance ProofWidgets.PenroseDiagramProps.instRpcEncodablePenroseDiagramProps : Lean.Server.RpcEncodable ProofWidgets.PenroseDiagramProps

Equations

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

def ProofWidgets.PenroseDiagram : ProofWidgets.Component ProofWidgets.PenroseDiagramProps

Displays the given diagram using Penrose. The website contains explanations of how to write domain (dsl), style (sty), and substance (sub) programs.

The diagram may also contain embedded HTML trees which are specified in embeds. Each embed is HTML together with the name of an object x in the substance program. The objhect x can be of any type but must be assigned an x.textBox : Rectangle field in the style program. This rectangle will be replaced with the HTML tree.

The following additional constants are prepended to the style program:

theme {
  color foreground
  color tooltipBackground
  color tooltipForeground
  color tooltipBorder
}

and can be accessed as, for example, theme.foreground in the provided sty in order to match the editor theme.

Equations

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