Skip to content

Commit 421d5c7

Browse files
mars0iMarshall AbramsVtec234
authored
Added axis type to Recharts.lean, modified Plot.lean to illustrate. (#99)
* Added axis type to Recharts.lean, modified Plot.lean to illustrate. * Committing package-lock.json cache files See https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/lake.20update's.20.20widget.2Fpackage-lock.2Ejson.2E*.20in.20ProofWidgets4.3F/near/490592688 * Modified the release URL * Apply suggestions from code review * chore: revert some changes --------- Co-authored-by: Marshall Abrams <marshall@logical.net> Co-authored-by: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>
1 parent 739763d commit 421d5c7

File tree

2 files changed

+11
-1
lines changed

2 files changed

+11
-1
lines changed

ProofWidgets/Component/Recharts.lean

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,20 @@ def LineChart : Component LineChartProps where
3838
javascript := Recharts.javascript
3939
«export» := "LineChart"
4040

41+
inductive AxisType where
42+
/-- Treat values as numbers: spacing on axis by numeric difference. -/
43+
| number
44+
/-- Treat values as categorical: equal spacing between values. -/
45+
| category
46+
deriving FromJson, ToJson
47+
4148
structure AxisProps where
4249
dataKey? : Option Json := none
4350
domain? : Option (Array Json) := none
4451
allowDataOverflow : Bool := false
52+
/-- How values along this axis should be interpreted.
53+
The Recharts default is `category`. -/
54+
type : AxisType := .number
4555
-- TODO: There are many more props
4656
deriving FromJson, ToJson
4757

widget/package-lock.json.trace

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)