def ProofWidgets.GraphDisplay.mkCircle (attrs : Array (String × Lean.Json) := #[]) : Html

A themed <circle> SVG element, with optional extra attributes.

Equations

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

inductive ProofWidgets.GraphDisplay.BoundingShape : Type

A shape containing the vertex label. Used to position incident edge endpoints. The shape is assumed to be centred on the vertex position.

• circle (radius : Float) : BoundingShape

  A circle of fixed radius.

• rect (width height : Float) : BoundingShape

  A rectangle of fixed dimensions.

instance ProofWidgets.GraphDisplay.instInhabitedBoundingShape : Inhabited BoundingShape

Equations

• ProofWidgets.GraphDisplay.instInhabitedBoundingShape = { default := ProofWidgets.GraphDisplay.BoundingShape.circle default }

instance ProofWidgets.GraphDisplay.instFromJsonBoundingShape : Lean.FromJson BoundingShape

Equations

• ProofWidgets.GraphDisplay.instFromJsonBoundingShape = { fromJson? := ProofWidgets.GraphDisplay.fromJsonBoundingShape✝ }

instance ProofWidgets.GraphDisplay.instToJsonBoundingShape : Lean.ToJson BoundingShape

Equations

• ProofWidgets.GraphDisplay.instToJsonBoundingShape = { toJson := ProofWidgets.GraphDisplay.toJsonBoundingShape✝ }

structure ProofWidgets.GraphDisplay.Vertex : Type

• id : String

  Identifier for this vertex. Must be unique.

• label : Html

  The label is drawn at the vertex position. This must be an SVG element. Use <foreignObject> to draw non-SVG elements.

• boundingShape : BoundingShape
• details? : Option Html

  Details are shown below the graph display after the vertex label has been clicked. See also Props.showDetails.

instance ProofWidgets.GraphDisplay.instInhabitedVertex : Inhabited Vertex

Equations

• ProofWidgets.GraphDisplay.instInhabitedVertex = { default := { id := default, label := default, boundingShape := default, details? := default } }

instance ProofWidgets.GraphDisplay.instRpcEncodableVertex : Lean.Server.RpcEncodable Vertex

Equations

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

structure ProofWidgets.GraphDisplay.Edge : Type

• source : String

  Source vertex. Must match the id of one of the vertices.

• target : String

  Target vertex. Must match the id of one of the vertices.

• attrs : Array (String × Lean.Json)

  Extra attributes to set on the SVG <line> element representing this edge. See also Props.defaultEdgeAttrs.

• label? : Option Html

  If present, the label is shown over the edge midpoint. This must be an SVG element. Use <foreignObject> to draw non-SVG elements.

• details? : Option Html

  Details are shown below the graph display after the edge has been clicked. See also Props.showDetails.

instance ProofWidgets.GraphDisplay.instInhabitedEdge : Inhabited Edge

Equations

• ProofWidgets.GraphDisplay.instInhabitedEdge = { default := { source := default, target := default, attrs := default, label? := default, details? := default } }

instance ProofWidgets.GraphDisplay.instRpcEncodableEdge : Lean.Server.RpcEncodable Edge

Equations

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

structure ProofWidgets.GraphDisplay.ForceCenterParams : Type

• x? : Option Float
• y? : Option Float
• strength? : Option Float

instance ProofWidgets.GraphDisplay.instInhabitedForceCenterParams : Inhabited ForceCenterParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceCenterParams = { default := { x? := default, y? := default, strength? := default } }

instance ProofWidgets.GraphDisplay.instFromJsonForceCenterParams : Lean.FromJson ForceCenterParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceCenterParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceCenterParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceCenterParams : Lean.ToJson ForceCenterParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceCenterParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceCenterParams✝ }

structure ProofWidgets.GraphDisplay.ForceCollideParams : Type

• radius? : Option Float
• strength? : Option Float
• iterations? : Option Nat

instance ProofWidgets.GraphDisplay.instInhabitedForceCollideParams : Inhabited ForceCollideParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceCollideParams = { default := { radius? := default, strength? := default, iterations? := default } }

instance ProofWidgets.GraphDisplay.instFromJsonForceCollideParams : Lean.FromJson ForceCollideParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceCollideParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceCollideParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceCollideParams : Lean.ToJson ForceCollideParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceCollideParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceCollideParams✝ }

structure ProofWidgets.GraphDisplay.ForceLinkParams : Type

• distance? : Option Float
• strength? : Option Float
• iterations? : Option Nat

instance ProofWidgets.GraphDisplay.instInhabitedForceLinkParams : Inhabited ForceLinkParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceLinkParams = { default := { distance? := default, strength? := default, iterations? := default } }

instance ProofWidgets.GraphDisplay.instFromJsonForceLinkParams : Lean.FromJson ForceLinkParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceLinkParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceLinkParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceLinkParams : Lean.ToJson ForceLinkParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceLinkParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceLinkParams✝ }

structure ProofWidgets.GraphDisplay.ForceManyBodyParams : Type

• strength? : Option Float
• theta? : Option Float
• distanceMin? : Option Float
• distanceMax? : Option Float

instance ProofWidgets.GraphDisplay.instInhabitedForceManyBodyParams : Inhabited ForceManyBodyParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceManyBodyParams = { default := { strength? := default, theta? := default, distanceMin? := default, distanceMax? := default } }

instance ProofWidgets.GraphDisplay.instFromJsonForceManyBodyParams : Lean.FromJson ForceManyBodyParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceManyBodyParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceManyBodyParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceManyBodyParams : Lean.ToJson ForceManyBodyParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceManyBodyParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceManyBodyParams✝ }

structure ProofWidgets.GraphDisplay.ForceXParams : Type

• x? : Option Float
• strength? : Option Float

instance ProofWidgets.GraphDisplay.instInhabitedForceXParams : Inhabited ForceXParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceXParams = { default := { x? := default, strength? := default } }

instance ProofWidgets.GraphDisplay.instFromJsonForceXParams : Lean.FromJson ForceXParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceXParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceXParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceXParams : Lean.ToJson ForceXParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceXParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceXParams✝ }

structure ProofWidgets.GraphDisplay.ForceYParams : Type

• y? : Option Float
• strength? : Option Float

instance ProofWidgets.GraphDisplay.instInhabitedForceYParams : Inhabited ForceYParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceYParams = { default := { y? := default, strength? := default } }

instance ProofWidgets.GraphDisplay.instFromJsonForceYParams : Lean.FromJson ForceYParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceYParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceYParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceYParams : Lean.ToJson ForceYParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceYParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceYParams✝ }

structure ProofWidgets.GraphDisplay.ForceRadialParams : Type

• radius : Float
• x? : Option Float
• y? : Option Float
• strength? : Option Float

instance ProofWidgets.GraphDisplay.instInhabitedForceRadialParams : Inhabited ForceRadialParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceRadialParams = { default := { radius := default, x? := default, y? := default, strength? := default } }

instance ProofWidgets.GraphDisplay.instFromJsonForceRadialParams : Lean.FromJson ForceRadialParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceRadialParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceRadialParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceRadialParams : Lean.ToJson ForceRadialParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceRadialParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceRadialParams✝ }

inductive ProofWidgets.GraphDisplay.ForceParams : Type

Settings for the simulation of forces on vertices. See https://d3js.org/d3-force.

• center : ForceCenterParams → ForceParams
• collide : ForceCollideParams → ForceParams
• link : ForceLinkParams → ForceParams
• manyBody : ForceManyBodyParams → ForceParams
• x : ForceXParams → ForceParams
• y : ForceYParams → ForceParams
• radial : ForceRadialParams → ForceParams

instance ProofWidgets.GraphDisplay.instInhabitedForceParams : Inhabited ForceParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceParams = { default := ProofWidgets.GraphDisplay.ForceParams.center default }

instance ProofWidgets.GraphDisplay.instFromJsonForceParams : Lean.FromJson ForceParams

Equations

• ProofWidgets.GraphDisplay.instFromJsonForceParams = { fromJson? := ProofWidgets.GraphDisplay.fromJsonForceParams✝ }

instance ProofWidgets.GraphDisplay.instToJsonForceParams : Lean.ToJson ForceParams

Equations

• ProofWidgets.GraphDisplay.instToJsonForceParams = { toJson := ProofWidgets.GraphDisplay.toJsonForceParams✝ }

structure ProofWidgets.GraphDisplay.Props : Type

• vertices : Array Vertex
• edges : Array Edge

  At most one edge may exist between any two vertices. Self-loops are allowed, but (TODO) are currently not rendered well.

• defaultEdgeAttrs : Array (String × Lean.Json)

  Attributes to set by default on <line> elements representing edges.

• forces : Array ForceParams

  Which forces to apply to the vertices. Most force parameters are optional, using default values if not specified.

• showDetails : Bool

  Whether to show a details box below the graph.

instance ProofWidgets.GraphDisplay.instInhabitedProps : Inhabited Props

Equations

• ProofWidgets.GraphDisplay.instInhabitedProps = { default := { vertices := default, edges := default, defaultEdgeAttrs := default, forces := default, showDetails := default } }

instance ProofWidgets.GraphDisplay.instRpcEncodableProps : Lean.Server.RpcEncodable Props

Equations

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

def ProofWidgets.GraphDisplay : Component GraphDisplay.Props

Display a graph with an interactive force simulation.

Equations

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