def ProofWidgets.Recharts.Recharts : Lean.Widget.Module

Equations

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

inductive ProofWidgets.Recharts.LineChartLayout : Type

• horizontal : LineChartLayout
• vertical : LineChartLayout

def ProofWidgets.Recharts.instFromJsonLineChartLayout.fromJson : Lean.Json → Except String LineChartLayout

Equations

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

instance ProofWidgets.Recharts.instFromJsonLineChartLayout : Lean.FromJson LineChartLayout

Equations

• ProofWidgets.Recharts.instFromJsonLineChartLayout = { fromJson? := ProofWidgets.Recharts.instFromJsonLineChartLayout.fromJson }

instance ProofWidgets.Recharts.instToJsonLineChartLayout : Lean.ToJson LineChartLayout

Equations

• ProofWidgets.Recharts.instToJsonLineChartLayout = { toJson := ProofWidgets.Recharts.instToJsonLineChartLayout.toJson }

def ProofWidgets.Recharts.instToJsonLineChartLayout.toJson : LineChartLayout → Lean.Json

Equations

• ProofWidgets.Recharts.instToJsonLineChartLayout.toJson ProofWidgets.Recharts.LineChartLayout.horizontal = Lean.toJson "horizontal"
• ProofWidgets.Recharts.instToJsonLineChartLayout.toJson ProofWidgets.Recharts.LineChartLayout.vertical = Lean.toJson "vertical"

inductive ProofWidgets.Recharts.LineChartSyncMethod : Type

• index : LineChartSyncMethod
• value : LineChartSyncMethod

instance ProofWidgets.Recharts.instFromJsonLineChartSyncMethod : Lean.FromJson LineChartSyncMethod

Equations

• ProofWidgets.Recharts.instFromJsonLineChartSyncMethod = { fromJson? := ProofWidgets.Recharts.instFromJsonLineChartSyncMethod.fromJson }

def ProofWidgets.Recharts.instFromJsonLineChartSyncMethod.fromJson : Lean.Json → Except String LineChartSyncMethod

Equations

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

instance ProofWidgets.Recharts.instToJsonLineChartSyncMethod : Lean.ToJson LineChartSyncMethod

Equations

• ProofWidgets.Recharts.instToJsonLineChartSyncMethod = { toJson := ProofWidgets.Recharts.instToJsonLineChartSyncMethod.toJson }

def ProofWidgets.Recharts.instToJsonLineChartSyncMethod.toJson : LineChartSyncMethod → Lean.Json

Equations

• ProofWidgets.Recharts.instToJsonLineChartSyncMethod.toJson ProofWidgets.Recharts.LineChartSyncMethod.index = Lean.toJson "index"
• ProofWidgets.Recharts.instToJsonLineChartSyncMethod.toJson ProofWidgets.Recharts.LineChartSyncMethod.value = Lean.toJson "value"

structure ProofWidgets.Recharts.LineChartMargin : Type

• top : Nat
• right : Nat
• bottom : Nat
• left : Nat

def ProofWidgets.Recharts.instFromJsonLineChartMargin.fromJson : Lean.Json → Except String LineChartMargin

Equations

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

instance ProofWidgets.Recharts.instFromJsonLineChartMargin : Lean.FromJson LineChartMargin

Equations

• ProofWidgets.Recharts.instFromJsonLineChartMargin = { fromJson? := ProofWidgets.Recharts.instFromJsonLineChartMargin.fromJson }

instance ProofWidgets.Recharts.instToJsonLineChartMargin : Lean.ToJson LineChartMargin

Equations

• ProofWidgets.Recharts.instToJsonLineChartMargin = { toJson := ProofWidgets.Recharts.instToJsonLineChartMargin.toJson }

def ProofWidgets.Recharts.instToJsonLineChartMargin.toJson : LineChartMargin → Lean.Json

Equations

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

structure ProofWidgets.Recharts.LineChartProps : Type

• layout : LineChartLayout
• syncId? : Option String
• syncMethod? : Option LineChartSyncMethod
• width : Nat
• height : Nat
• data : Array Lean.Json
• margin : LineChartMargin

instance ProofWidgets.Recharts.instFromJsonLineChartProps : Lean.FromJson LineChartProps

Equations

• ProofWidgets.Recharts.instFromJsonLineChartProps = { fromJson? := ProofWidgets.Recharts.instFromJsonLineChartProps.fromJson }

def ProofWidgets.Recharts.instFromJsonLineChartProps.fromJson : Lean.Json → Except String LineChartProps

Equations

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

instance ProofWidgets.Recharts.instToJsonLineChartProps : Lean.ToJson LineChartProps

Equations

• ProofWidgets.Recharts.instToJsonLineChartProps = { toJson := ProofWidgets.Recharts.instToJsonLineChartProps.toJson }

def ProofWidgets.Recharts.instToJsonLineChartProps.toJson : LineChartProps → Lean.Json

Equations

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

def ProofWidgets.Recharts.LineChart : Component LineChartProps

See https://recharts.org/en-US/api/LineChart.

Equations

• ProofWidgets.Recharts.LineChart = { javascript := ProofWidgets.Recharts.Recharts.javascript, «export» := "LineChart" }

inductive ProofWidgets.Recharts.AxisType : Type

• number : AxisType

  Treat values as numbers: spacing on axis by numeric difference.

• category : AxisType

  Treat values as categorical: equal spacing between values.

def ProofWidgets.Recharts.instFromJsonAxisType.fromJson : Lean.Json → Except String AxisType

Equations

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

instance ProofWidgets.Recharts.instFromJsonAxisType : Lean.FromJson AxisType

Equations

• ProofWidgets.Recharts.instFromJsonAxisType = { fromJson? := ProofWidgets.Recharts.instFromJsonAxisType.fromJson }

def ProofWidgets.Recharts.instToJsonAxisType.toJson : AxisType → Lean.Json

Equations

• ProofWidgets.Recharts.instToJsonAxisType.toJson ProofWidgets.Recharts.AxisType.number = Lean.toJson "number"
• ProofWidgets.Recharts.instToJsonAxisType.toJson ProofWidgets.Recharts.AxisType.category = Lean.toJson "category"

instance ProofWidgets.Recharts.instToJsonAxisType : Lean.ToJson AxisType

Equations

• ProofWidgets.Recharts.instToJsonAxisType = { toJson := ProofWidgets.Recharts.instToJsonAxisType.toJson }

structure ProofWidgets.Recharts.AxisProps : Type

• dataKey? : Option Lean.Json
• domain? : Option (Array Lean.Json)
• allowDataOverflow : Bool
• type : AxisType

  How values along this axis should be interpreted. The Recharts default is category.

def ProofWidgets.Recharts.instFromJsonAxisProps.fromJson : Lean.Json → Except String AxisProps

Equations

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

instance ProofWidgets.Recharts.instFromJsonAxisProps : Lean.FromJson AxisProps

Equations

• ProofWidgets.Recharts.instFromJsonAxisProps = { fromJson? := ProofWidgets.Recharts.instFromJsonAxisProps.fromJson }

instance ProofWidgets.Recharts.instToJsonAxisProps : Lean.ToJson AxisProps

Equations

• ProofWidgets.Recharts.instToJsonAxisProps = { toJson := ProofWidgets.Recharts.instToJsonAxisProps.toJson }

def ProofWidgets.Recharts.instToJsonAxisProps.toJson : AxisProps → Lean.Json

Equations

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

def ProofWidgets.Recharts.XAxis : Component AxisProps

See https://recharts.org/en-US/api/XAxis.

Equations

• ProofWidgets.Recharts.XAxis = { javascript := ProofWidgets.Recharts.Recharts.javascript, «export» := "XAxis" }

def ProofWidgets.Recharts.YAxis : Component AxisProps

See https://recharts.org/en-US/api/YAxis.

Equations

• ProofWidgets.Recharts.YAxis = { javascript := ProofWidgets.Recharts.Recharts.javascript, «export» := "YAxis" }

inductive ProofWidgets.Recharts.LineType : Type

• basis : LineType
• basisClosed : LineType
• basisOpen : LineType
• linear : LineType
• linearClosed : LineType
• natural : LineType
• monotoneX : LineType
• monotoneY : LineType
• monotone : LineType
• step : LineType
• stepBefore : LineType
• stepAfter : LineType

def ProofWidgets.Recharts.instFromJsonLineType.fromJson : Lean.Json → Except String LineType

Equations

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

instance ProofWidgets.Recharts.instFromJsonLineType : Lean.FromJson LineType

Equations

• ProofWidgets.Recharts.instFromJsonLineType = { fromJson? := ProofWidgets.Recharts.instFromJsonLineType.fromJson }

instance ProofWidgets.Recharts.instToJsonLineType : Lean.ToJson LineType

Equations

• ProofWidgets.Recharts.instToJsonLineType = { toJson := ProofWidgets.Recharts.instToJsonLineType.toJson }

def ProofWidgets.Recharts.instToJsonLineType.toJson : LineType → Lean.Json

Equations

• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.basis = Lean.toJson "basis"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.basisClosed = Lean.toJson "basisClosed"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.basisOpen = Lean.toJson "basisOpen"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.linear = Lean.toJson "linear"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.linearClosed = Lean.toJson "linearClosed"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.natural = Lean.toJson "natural"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.monotoneX = Lean.toJson "monotoneX"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.monotoneY = Lean.toJson "monotoneY"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.monotone = Lean.toJson "monotone"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.step = Lean.toJson "step"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.stepBefore = Lean.toJson "stepBefore"
• ProofWidgets.Recharts.instToJsonLineType.toJson ProofWidgets.Recharts.LineType.stepAfter = Lean.toJson "stepAfter"

structure ProofWidgets.Recharts.LineProps : Type

• type : LineType
• dataKey : Lean.Json
• stroke : String
• dot? : Option Bool

instance ProofWidgets.Recharts.instFromJsonLineProps : Lean.FromJson LineProps

Equations

• ProofWidgets.Recharts.instFromJsonLineProps = { fromJson? := ProofWidgets.Recharts.instFromJsonLineProps.fromJson }

def ProofWidgets.Recharts.instFromJsonLineProps.fromJson : Lean.Json → Except String LineProps

Equations

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

instance ProofWidgets.Recharts.instToJsonLineProps : Lean.ToJson LineProps

Equations

• ProofWidgets.Recharts.instToJsonLineProps = { toJson := ProofWidgets.Recharts.instToJsonLineProps.toJson }

def ProofWidgets.Recharts.instToJsonLineProps.toJson : LineProps → Lean.Json

Equations

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

def ProofWidgets.Recharts.Line : Component LineProps

See https://recharts.org/en-US/api/Line.

Equations

• ProofWidgets.Recharts.Line = { javascript := ProofWidgets.Recharts.Recharts.javascript, «export» := "Line" }