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.

def ProofWidgets.GraphDisplay.instInhabitedBoundingShape.default : BoundingShape

Equations

• ProofWidgets.GraphDisplay.instInhabitedBoundingShape.default = ProofWidgets.GraphDisplay.BoundingShape.circle default

instance ProofWidgets.GraphDisplay.instInhabitedBoundingShape : Inhabited BoundingShape

Equations

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

instance ProofWidgets.GraphDisplay.instFromJsonBoundingShape : Lean.FromJson BoundingShape

Equations

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

def ProofWidgets.GraphDisplay.instFromJsonBoundingShape.fromJson : Lean.Json → Except String BoundingShape

Equations

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

def ProofWidgets.GraphDisplay.instToJsonBoundingShape.toJson : BoundingShape → Lean.Json

Equations

• One or more equations did not get rendered due to their size.
• ProofWidgets.GraphDisplay.instToJsonBoundingShape.toJson (ProofWidgets.GraphDisplay.BoundingShape.circle a) = Lean.Json.mkObj [("circle", Lean.Json.mkObj [("radius", Lean.toJson a)])]

instance ProofWidgets.GraphDisplay.instToJsonBoundingShape : Lean.ToJson BoundingShape

Equations

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

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 := ProofWidgets.GraphDisplay.instInhabitedVertex.default }

def ProofWidgets.GraphDisplay.instInhabitedVertex.default : 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 := ProofWidgets.GraphDisplay.instInhabitedEdge.default }

def ProofWidgets.GraphDisplay.instInhabitedEdge.default : 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

def ProofWidgets.GraphDisplay.instInhabitedForceCenterParams.default : ForceCenterParams

Equations

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

instance ProofWidgets.GraphDisplay.instInhabitedForceCenterParams : Inhabited ForceCenterParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceCenterParams = { default := ProofWidgets.GraphDisplay.instInhabitedForceCenterParams.default }

def ProofWidgets.GraphDisplay.instFromJsonForceCenterParams.fromJson : Lean.Json → Except String ForceCenterParams

Equations

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

instance ProofWidgets.GraphDisplay.instFromJsonForceCenterParams : Lean.FromJson ForceCenterParams

Equations

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

instance ProofWidgets.GraphDisplay.instToJsonForceCenterParams : Lean.ToJson ForceCenterParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceCenterParams.toJson : ForceCenterParams → Lean.Json

Equations

• ProofWidgets.GraphDisplay.instToJsonForceCenterParams.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "x" x✝.x?, Lean.Json.opt "y" x✝.y?, Lean.Json.opt "strength" x✝.strength?].flatten

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 := ProofWidgets.GraphDisplay.instInhabitedForceCollideParams.default }

def ProofWidgets.GraphDisplay.instInhabitedForceCollideParams.default : ForceCollideParams

Equations

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

def ProofWidgets.GraphDisplay.instFromJsonForceCollideParams.fromJson : Lean.Json → Except String ForceCollideParams

Equations

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

instance ProofWidgets.GraphDisplay.instFromJsonForceCollideParams : Lean.FromJson ForceCollideParams

Equations

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

instance ProofWidgets.GraphDisplay.instToJsonForceCollideParams : Lean.ToJson ForceCollideParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceCollideParams.toJson : ForceCollideParams → Lean.Json

Equations

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

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 := ProofWidgets.GraphDisplay.instInhabitedForceLinkParams.default }

def ProofWidgets.GraphDisplay.instInhabitedForceLinkParams.default : 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.instFromJsonForceLinkParams.fromJson }

def ProofWidgets.GraphDisplay.instFromJsonForceLinkParams.fromJson : Lean.Json → Except String ForceLinkParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceLinkParams.toJson : ForceLinkParams → Lean.Json

Equations

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

instance ProofWidgets.GraphDisplay.instToJsonForceLinkParams : Lean.ToJson ForceLinkParams

Equations

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

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 := ProofWidgets.GraphDisplay.instInhabitedForceManyBodyParams.default }

def ProofWidgets.GraphDisplay.instInhabitedForceManyBodyParams.default : 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.instFromJsonForceManyBodyParams.fromJson }

def ProofWidgets.GraphDisplay.instFromJsonForceManyBodyParams.fromJson : Lean.Json → Except String ForceManyBodyParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceManyBodyParams.toJson : ForceManyBodyParams → Lean.Json

Equations

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

instance ProofWidgets.GraphDisplay.instToJsonForceManyBodyParams : Lean.ToJson ForceManyBodyParams

Equations

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

structure ProofWidgets.GraphDisplay.ForceXParams : Type

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

def ProofWidgets.GraphDisplay.instInhabitedForceXParams.default : ForceXParams

Equations

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

instance ProofWidgets.GraphDisplay.instInhabitedForceXParams : Inhabited ForceXParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceXParams = { default := ProofWidgets.GraphDisplay.instInhabitedForceXParams.default }

def ProofWidgets.GraphDisplay.instFromJsonForceXParams.fromJson : Lean.Json → Except String ForceXParams

Equations

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

instance ProofWidgets.GraphDisplay.instFromJsonForceXParams : Lean.FromJson ForceXParams

Equations

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

instance ProofWidgets.GraphDisplay.instToJsonForceXParams : Lean.ToJson ForceXParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceXParams.toJson : ForceXParams → Lean.Json

Equations

• ProofWidgets.GraphDisplay.instToJsonForceXParams.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "x" x✝.x?, Lean.Json.opt "strength" x✝.strength?].flatten

structure ProofWidgets.GraphDisplay.ForceYParams : Type

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

instance ProofWidgets.GraphDisplay.instInhabitedForceYParams : Inhabited ForceYParams

Equations

• ProofWidgets.GraphDisplay.instInhabitedForceYParams = { default := ProofWidgets.GraphDisplay.instInhabitedForceYParams.default }

def ProofWidgets.GraphDisplay.instInhabitedForceYParams.default : ForceYParams

Equations

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

instance ProofWidgets.GraphDisplay.instFromJsonForceYParams : Lean.FromJson ForceYParams

Equations

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

def ProofWidgets.GraphDisplay.instFromJsonForceYParams.fromJson : Lean.Json → Except String ForceYParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceYParams.toJson : ForceYParams → Lean.Json

Equations

• ProofWidgets.GraphDisplay.instToJsonForceYParams.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "y" x✝.y?, Lean.Json.opt "strength" x✝.strength?].flatten

instance ProofWidgets.GraphDisplay.instToJsonForceYParams : Lean.ToJson ForceYParams

Equations

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

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 := ProofWidgets.GraphDisplay.instInhabitedForceRadialParams.default }

def ProofWidgets.GraphDisplay.instInhabitedForceRadialParams.default : 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.instFromJsonForceRadialParams.fromJson }

def ProofWidgets.GraphDisplay.instFromJsonForceRadialParams.fromJson : Lean.Json → Except String ForceRadialParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceRadialParams.toJson : ForceRadialParams → Lean.Json

Equations

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

instance ProofWidgets.GraphDisplay.instToJsonForceRadialParams : Lean.ToJson ForceRadialParams

Equations

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

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.instInhabitedForceParams.default }

def ProofWidgets.GraphDisplay.instInhabitedForceParams.default : 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.instFromJsonForceParams.fromJson }

def ProofWidgets.GraphDisplay.instFromJsonForceParams.fromJson : Lean.Json → Except String ForceParams

Equations

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

instance ProofWidgets.GraphDisplay.instToJsonForceParams : Lean.ToJson ForceParams

Equations

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

def ProofWidgets.GraphDisplay.instToJsonForceParams.toJson : ForceParams → Lean.Json

Equations

• ProofWidgets.GraphDisplay.instToJsonForceParams.toJson (ProofWidgets.GraphDisplay.ForceParams.center a) = Lean.Json.mkObj [("center", Lean.toJson a)]
• ProofWidgets.GraphDisplay.instToJsonForceParams.toJson (ProofWidgets.GraphDisplay.ForceParams.collide a) = Lean.Json.mkObj [("collide", Lean.toJson a)]
• ProofWidgets.GraphDisplay.instToJsonForceParams.toJson (ProofWidgets.GraphDisplay.ForceParams.link a) = Lean.Json.mkObj [("link", Lean.toJson a)]
• ProofWidgets.GraphDisplay.instToJsonForceParams.toJson (ProofWidgets.GraphDisplay.ForceParams.manyBody a) = Lean.Json.mkObj [("manyBody", Lean.toJson a)]
• ProofWidgets.GraphDisplay.instToJsonForceParams.toJson (ProofWidgets.GraphDisplay.ForceParams.x a) = Lean.Json.mkObj [("x", Lean.toJson a)]
• ProofWidgets.GraphDisplay.instToJsonForceParams.toJson (ProofWidgets.GraphDisplay.ForceParams.y a) = Lean.Json.mkObj [("y", Lean.toJson a)]
• ProofWidgets.GraphDisplay.instToJsonForceParams.toJson (ProofWidgets.GraphDisplay.ForceParams.radial a) = Lean.Json.mkObj [("radial", Lean.toJson a)]

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 := ProofWidgets.GraphDisplay.instInhabitedProps.default }

def ProofWidgets.GraphDisplay.instInhabitedProps.default : 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.