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

instance ProofWidgets.Recharts.instFromJsonLineChartLayout : Lean.FromJson LineChartLayout

Equations

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

instance ProofWidgets.Recharts.instToJsonLineChartLayout : Lean.ToJson LineChartLayout

Equations

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

inductive ProofWidgets.Recharts.LineChartSyncMethod : Type

• index : LineChartSyncMethod
• value : LineChartSyncMethod

instance ProofWidgets.Recharts.instFromJsonLineChartSyncMethod : Lean.FromJson LineChartSyncMethod

Equations

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

instance ProofWidgets.Recharts.instToJsonLineChartSyncMethod : Lean.ToJson LineChartSyncMethod

Equations

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

structure ProofWidgets.Recharts.LineChartMargin : Type

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

instance ProofWidgets.Recharts.instFromJsonLineChartMargin : Lean.FromJson LineChartMargin

Equations

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

instance ProofWidgets.Recharts.instToJsonLineChartMargin : Lean.ToJson LineChartMargin

Equations

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

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.fromJsonLineChartProps✝ }

instance ProofWidgets.Recharts.instToJsonLineChartProps : Lean.ToJson LineChartProps

Equations

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

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.

instance ProofWidgets.Recharts.instFromJsonAxisType : Lean.FromJson AxisType

Equations

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

instance ProofWidgets.Recharts.instToJsonAxisType : Lean.ToJson AxisType

Equations

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

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.

instance ProofWidgets.Recharts.instFromJsonAxisProps : Lean.FromJson AxisProps

Equations

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

instance ProofWidgets.Recharts.instToJsonAxisProps : Lean.ToJson AxisProps

Equations

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

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

instance ProofWidgets.Recharts.instFromJsonLineType : Lean.FromJson LineType

Equations

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

instance ProofWidgets.Recharts.instToJsonLineType : Lean.ToJson LineType

Equations

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

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.fromJsonLineProps✝ }

instance ProofWidgets.Recharts.instToJsonLineProps : Lean.ToJson LineProps

Equations

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

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" }