-
Notifications
You must be signed in to change notification settings - Fork 23
/
Recharts.lean
76 lines (62 loc) · 1.96 KB
/
Recharts.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
import ProofWidgets.Component.Basic
namespace ProofWidgets.Recharts
open Lean
@[widget_module]
def Recharts : Widget.Module where
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "recharts.js"
inductive LineChartLayout where
| horizontal
| vertical
deriving FromJson, ToJson
inductive LineChartSyncMethod where
| index | value
deriving FromJson, ToJson
structure LineChartMargin where
top : Nat := 5
right : Nat := 5
bottom : Nat := 5
left : Nat := 5
deriving FromJson, ToJson
structure LineChartProps where
layout : LineChartLayout := .horizontal
syncId? : Option String := none
syncMethod? : Option LineChartSyncMethod := some .index
width : Nat
height : Nat
data : Array Json
margin : LineChartMargin := {}
deriving FromJson, ToJson
/-- See https://recharts.org/en-US/api/LineChart. -/
def LineChart : Component LineChartProps where
javascript := Recharts.javascript
«export» := "LineChart"
structure AxisProps where
dataKey? : Option Json := none
domain? : Option (Array Json) := none
allowDataOverflow : Bool := false
-- TODO: There are many more props
deriving FromJson, ToJson
/-- See https://recharts.org/en-US/api/XAxis. -/
def XAxis : Component AxisProps where
javascript := Recharts.javascript
«export» := "XAxis"
/-- See https://recharts.org/en-US/api/YAxis. -/
def YAxis : Component AxisProps where
javascript := Recharts.javascript
«export» := "YAxis"
inductive LineType where
| basis | basisClosed | basisOpen | linear | linearClosed | natural | monotoneX | monotoneY
| monotone | step | stepBefore | stepAfter
deriving FromJson, ToJson
structure LineProps where
type : LineType := .linear
dataKey : Json
stroke : String
dot? : Option Bool := none
-- TODO: There are many more props
deriving FromJson, ToJson
/-- See https://recharts.org/en-US/api/Line. -/
def Line : Component LineProps where
javascript := Recharts.javascript
«export» := "Line"
end ProofWidgets.Recharts