inductive ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine : Type

Layout engine used by Graphviz. See https://www.graphviz.org/docs/layouts/.

• circo : GraphvizLayoutEngine
• dot : GraphvizLayoutEngine
• fdp : GraphvizLayoutEngine
• sfdp : GraphvizLayoutEngine
• neato : GraphvizLayoutEngine
• osage : GraphvizLayoutEngine
• patchwork : GraphvizLayoutEngine
• twopi : GraphvizLayoutEngine

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instInhabitedGraphvizLayoutEngine : Inhabited GraphvizLayoutEngine

Equations

• ProofWidgets.GraphvizDisplay.instInhabitedGraphvizLayoutEngine = { default := ProofWidgets.GraphvizDisplay.instInhabitedGraphvizLayoutEngine.default }

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instFromJsonGraphvizLayoutEngine : Lean.FromJson GraphvizLayoutEngine

Equations

• ProofWidgets.GraphvizDisplay.instFromJsonGraphvizLayoutEngine = { fromJson? := ProofWidgets.GraphvizDisplay.instFromJsonGraphvizLayoutEngine.fromJson }

def ProofWidgets.GraphvizDisplay.instFromJsonGraphvizLayoutEngine.fromJson : Lean.Json → Except String GraphvizLayoutEngine

Equations

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

def ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson : GraphvizLayoutEngine → Lean.Json

Equations

• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.circo = Lean.toJson "circo"
• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.dot = Lean.toJson "dot"
• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.fdp = Lean.toJson "fdp"
• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.sfdp = Lean.toJson "sfdp"
• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.neato = Lean.toJson "neato"
• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.osage = Lean.toJson "osage"
• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.patchwork = Lean.toJson "patchwork"
• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson ProofWidgets.GraphvizDisplay.GraphvizLayoutEngine.twopi = Lean.toJson "twopi"

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine : Lean.ToJson GraphvizLayoutEngine

Equations

• ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine = { toJson := ProofWidgets.GraphvizDisplay.instToJsonGraphvizLayoutEngine.toJson }

structure ProofWidgets.GraphvizDisplay.D3GraphvizOptions : Type

Options passed to the d3-graphviz renderer. See https://github.com/magjac/d3-graphviz#selection_graphviz.

• useWorker? : Option Bool
• engine? : Option GraphvizLayoutEngine
• totalMemory? : Option Float
• fade? : Option Bool
• tweenPaths? : Option Bool
• tweenShapes? : Option Bool
• convertEqualSidedPolygons? : Option Bool
• tweenPrecision? : Option Lean.Json

  d3-graphviz accepts number | string.

• growEnteringEdges? : Option Bool
• zoom? : Option Bool
• zoomScaleExtent? : Option (Float × Float)
• zoomTranslateExtent? : Option ((Float × Float) × Float × Float)
• width? : Option Float

  If not provided, the SVG dynamically resizes to its parent div's width.

• height? : Option Float

  If not provided, the SVG dynamically resizes to its parent div's width.

• scale? : Option Float
• fit? : Option Bool

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instInhabitedD3GraphvizOptions : Inhabited D3GraphvizOptions

Equations

• ProofWidgets.GraphvizDisplay.instInhabitedD3GraphvizOptions = { default := ProofWidgets.GraphvizDisplay.instInhabitedD3GraphvizOptions.default }

def ProofWidgets.GraphvizDisplay.instFromJsonD3GraphvizOptions.fromJson : Lean.Json → Except String D3GraphvizOptions

Equations

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

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instFromJsonD3GraphvizOptions : Lean.FromJson D3GraphvizOptions

Equations

• ProofWidgets.GraphvizDisplay.instFromJsonD3GraphvizOptions = { fromJson? := ProofWidgets.GraphvizDisplay.instFromJsonD3GraphvizOptions.fromJson }

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instToJsonD3GraphvizOptions : Lean.ToJson D3GraphvizOptions

Equations

• ProofWidgets.GraphvizDisplay.instToJsonD3GraphvizOptions = { toJson := ProofWidgets.GraphvizDisplay.instToJsonD3GraphvizOptions.toJson }

def ProofWidgets.GraphvizDisplay.instToJsonD3GraphvizOptions.toJson : D3GraphvizOptions → Lean.Json

Equations

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

structure ProofWidgets.GraphvizDisplay.Props : Type

• dot : String

  Graphviz source of the graph.

• options : D3GraphvizOptions
• renderDebounceMs : Nat

  How long to wait before re-rendering the graph when the target SVG size changes. Larger graphs should use longer timeouts to avoid many expensive re-renders.

• className? : Option String

  Additional classes to place on the SVG's parent div.

• style? : Option Lean.Json

  Additional styling to place on the SVG's parent div.

• centerOnVertex? : Option String

  Center the display on the vertex with the given Graphviz node ID whenever this prop changes, including on initial render.

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instInhabitedProps : Inhabited Props

Equations

• ProofWidgets.GraphvizDisplay.instInhabitedProps = { default := ProofWidgets.GraphvizDisplay.instInhabitedProps.default }

def ProofWidgets.GraphvizDisplay.instFromJsonProps.fromJson : Lean.Json → Except String Props

Equations

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

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instFromJsonProps : Lean.FromJson Props

Equations

• ProofWidgets.GraphvizDisplay.instFromJsonProps = { fromJson? := ProofWidgets.GraphvizDisplay.instFromJsonProps.fromJson }

def ProofWidgets.GraphvizDisplay.instToJsonProps.toJson : Props → Lean.Json

Equations

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

@[instance_reducible]

instance ProofWidgets.GraphvizDisplay.instToJsonProps : Lean.ToJson Props

Equations

• ProofWidgets.GraphvizDisplay.instToJsonProps = { toJson := ProofWidgets.GraphvizDisplay.instToJsonProps.toJson }

def ProofWidgets.GraphvizDisplay : Component GraphvizDisplay.Props

Renders a graph from a Graphviz source string.

Equations

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