Overlay operators (*) (/) and operator demo

.cursor/rules/debug-chart-images.mdc

@@ -0,0 +1,14 @@
+---
+description: debugging, plotting
+globs: 
+alwaysApply: false
+---
+# Debugging Charts with Image Snapshots
+
+When you are **debugging a new chart component** or tweaking visual details, generate a quick PNG snapshot so you can inspect the exact rendering independent of VS Code's Infoview.
+
+* Use the existing `mcp_Playwright_playwright_screenshot` tool or `Recharts`' built-in export.
+* Save images under `docs/img/` with the naming scheme `<Module>-<Feature>-<step>.png`.
+* Link the snapshot from the relevant Markdown docs (e.g. [`README.md`](mdc:README.md) or [`Gallery.md`](mdc:Gallery.md)) so future contributors can see the before/after.
+
+This practice helps catch off-by-one pixel issues and colour-palette regressions that are hard to notice in the live preview alone.

.cursor/rules/lean-import-order.mdc

@@ -0,0 +1,42 @@
+---
+description: 
+globs: /**/*.lean,*.lean,**.lean
+alwaysApply: false
+---
+# Lean Import Ordering and Doc Comment Rules
+
+In Lean 4, `import` commands **must** appear *before* any other syntax items **including** module comments (`/-! … -/`) and doc comments (`/-- … -/`). Additionally, `import`, `namespace`, and `section` declarations themselves **cannot** carry doc comments.
+
+## Guidelines
+
+- Place the complete block of `import` statements at the very top of every `.lean` file.
+- Follow the imports with an optional *module comment* (`/-! … -/`) that documents the purpose of the file.
+- Do **not** attach doc comments to `import`, `namespace`, or `section` declarations; comment on the items *inside* the namespace/section instead.
+
+### ✅ Correct
+```lean
+import Mathlib.Data.Real.Basic
+import LeanPlot.API
+
+/-!
+# Module description
+This file …
+-/
+
+namespace Foo
+
+-- definitions …
+
+end Foo
+```
+
+### ❌ Incorrect
+```lean
+/-!
+# Module description
+This file …
+-/
+import LeanPlot.API  -- ERROR: import after comment
+```
+
+Adhering to these rules prevents `invalid 'import' command` errors and keeps file structure consistent across the codebase.

.cursor/rules/plot-feature-gallery.mdc

@@ -0,0 +1,10 @@
+---
+description:
+globs:
+alwaysApply: false
+---
+# Gallery Example Rule
+
+Whenever you implement **any new plot feature or chart type** in LeanPlot, add a corresponding demo entry to the gallery so users can discover it quickly.
+
+The demo should live under `LeanPlot/Demos/` and be linked in [Gallery.md](mdc:Gallery.md).  Prefer the naming convention `<FeatureName>Demo.lean`.

.cursor/rules/verso-docstrings.mdc

@@ -0,0 +1,55 @@
+---
+description: 
+globs: 
+alwaysApply: false
+---
+# Verso Docstring & Manual Generation Guide
+
+This repository uses **Verso** (see dependency declared in `lakefile.toml`) to build interactive manuals and API docs directly from Lean code.
+
+## High-level pipeline
+
+1. **Environment preparation** – every constant that should be documented must be `import`-ed so it is present in the Lean environment that Verso runs in.
+2. **Extraction** – VersoManual's helper `Verso.Genre.Manual.getDocString?` wraps Lean's `findDocString?` to pull doc comments and apply policy checks (missing / deprecated docs ⇒ errors unless options allow).
+3. **Representation in AST** – a docstring becomes a custom block node:
+   ```lean
+   Block.docstring
+   name := `Verso.Genre.Manual.Block.docstring
+   data := toJson (declName, declType, signature, customLabel?)
+   ```
+4. **Traversal hooks** – the block extension (`@[block_extension Block.docstring]` in `VersoManual/Docstring.lean`) registers each constant in the `docstringDomain`.  This enables hyperlinks `{docstring Foo.bar}` inside prose.
+5. **HTML renderer** – `toHtml` prettifies signature + markdown, adds hover cards, and injects into the generated manual page.
+
+## Key modules to read (paths are *inside the Verso vendored source*)
+* [`VersoManual/Docstring.lean`](mdc:.lake/packages/verso/src/verso-manual/VersoManual/Docstring.lean) – extraction, block definition, traversal, renderer
+* [`VersoManual/InlineLean.lean`](mdc:.lake/packages/verso/src/verso-manual/VersoManual/InlineLean.lean) – inline role `{docstring …}` expander (~line 730)
+* [`VersoManual/Docstring/Config.lean`](mdc:.lake/packages/verso/src/verso-manual/VersoManual/Docstring/Config.lean) – user-options controlling strictness
+
+## Options (can be set with `set_option` before running docs build)
+| Option | Default | Effect |
+| --- | --- | --- |
+| `verso.docstring.allowMissing` | `true` | Warn vs error on missing docs |
+| `verso.docstring.allowDeprecated` | `false` | Allow documenting deprecated names |
+| `verso.docstring.elabMarkdown` | `true` | Elaborate Lean snippets inside markdown |
+
+## Using in LeanPlot
+
+Create a manual executable (see `DocsMain.lean` plan) that `import`s both your library and VersoManual:
+```lean
+import LeanPlot
+import VersoManual
+
+def book : Book := -- assemble chapters, can use `{docstring Foo}` links
+
+def main : IO Unit := manualMain Theme.default book
+```
+Run `lake exe docs --output _docs` to generate static HTML with fully linked and linted API reference.
+
+## Lint policy
+
+CI should run the docs build.  If a public constant lacks `/- … -/` documentation and `verso.docstring.allowMissing` is `false` the build fails, ensuring documentation coverage.
+
+> Tip: You can quickly locate missing docs during development by generating a **draft** build (`--depth draft` flag in reference-manual) which shows coverage bars.
+
+---
+This rule helps future AI agents navigate Verso's docstring machinery and avoid re-discovering the same patterns.

.cursorrules

@@ -4,9 +4,9 @@ Install it (I have npm, so that's not an issue). They have some Recharts integra
 
 checklist (fill in as you go):
 
-- [ ] y = x
-- [ ] y=x^2
-- [ ] multiple plots in one graph
+- [x] y = x
+- [x] y=x^2
+- [x] multiple plots in one graph
 
 Base everything on floats in the end.
 

CHANGELOG.md

@@ -1,20 +1,119 @@
+# Changelog
+
 ## [0.1.0] – 2025-05-01:20:15
+
 ### Added
+
 - Initial roadmap and design plan for LeanPlot library
 - Basic demo overlay of y=x and y=x^2 via Recharts in ProofWidgets
 
 ### Planned
+
 - Abstract sampling helpers (`sample`, `sampleMany`)
 - Chart builder `mkLineChart`
-- Documentation updates 
+- Documentation updates
 
 ## [0.1.1] – 2025-05-02:07:41
+
 ### Added
+
 - `ToFloat` typeclass providing a uniform conversion **to `Float`** for numeric-like types (`Float`, `Nat`, `Int` instances implemented; `Rat` stubbed).
 - Generalised `LeanPlot.Components.sample` and `sampleMany` to work with any codomain that has a `[ToFloat]` instance.
 
 ### Changed
+
 - `LeanPlot.Demos.overlay` now relies on the `sampleMany` helper instead of a bespoke sampler.
 
 ### Breaking
-- Call-sites of `sample` & `sampleMany` must supply functions returning a type with a `[ToFloat]` instance. Existing `Float` code is unaffected. 
+
+- Call-sites of `sample` & `sampleMany` must supply functions returning a type with a `[ToFloat]` instance. Existing `Float` code is unaffected.
+
+## [0.1.2] – 2025-05-02:08:05
+
+### Added
+
+- `LeanPlot.Legend` exposing the Recharts `<Legend>` component.
+- `mkLineChartFull` helper that embeds a legend automatically.
+- `#plot` command (alias of `#html`) via `LeanPlot.PlotCommand`.
+- Demo `LeanPlot.Demos.LinearDemo` now uses `#plot`.
+
+### Changed
+
+- Root `LeanPlot` module imports new `Plot` command.
+- Updated TODO roadmap with ergonomics and grammar-of-graphics sections.
+
+### Fixed
+
+- N/A
+
+## [0.1.3] – 2025-05-02:08:12
+
+### Added
+
+- New demo `LeanPlot.Demos.QuadraticDemo` (`y = x²`).
+- New demo `LeanPlot.Demos.OverlayDemo` demonstrating multi-series overlay with legend.
+
+### Changed
+
+- `Gallery.md` line-chart checklist now ticks off linear and quadratic demos.
+
+## [0.2.0] – 2025-05-03:09:41
+
+### Added
+
+- Tier-0 ergonomics layer: new module `LeanPlot.API` with zero-config helpers
+  - `lineChart` – sample a `Float → β` function on `[0,1]` and render.
+  - `scatterChart` – render array of points (first implementation via `mkScatterChart`).
+- Core `LeanPlot.Components` now includes bindings for Recharts `ScatterChart`/`Scatter` and helper `mkScatterChart`.
+- Library-wide defaults centralised in `LeanPlot.Constants` (`defaultW`, `defaultH`).
+
+### Changed
+
+- Palette helpers now expose `colourFor` for single series selection.
+
+### Fixed
+
+- None.
+
+## [0.2.1] – 2025-05-03:10:25
+
+### Changed
+
+- Introduced `LeanPlot.Core` with the general `Render`, `Layer`, `Plot` abstractions.
+- Added low-priority generic `HAdd` instance that overlays any `[ToPlot]` values via `Plot.overlay`.
+- Migrated `LeanPlot.Algebra` to these abstractions, deleting duplicated `Render`/`CoeTC` and bespoke `HAdd`.
+- `LinePlot` now only provides a `[ToLayer]` instance and inherits `+` overlay behaviour from the core instance.
+
+## [0.2.2] – 2025-05-07:19:00
+
+### Added
+
+- **Warning Banner for Invalid Plot Data**: Charts now display a warning banner if the input data contains `NaN` or `Infinity` values. This helps users identify problematic data that might lead to incorrect or empty plots.
+  - New `LeanPlot.WarningBanner` component for displaying HTML-based warnings.
+  - New utility functions in `LeanPlot.Utils` (`isInvalidFloat`, `jsonDataHasInvalidFloats`) to detect invalid floating-point numbers in JSON data.
+  - Chart generation functions in `LeanPlot.Components` (e.g., `mkLineChart`, `mkScatterChart`) now integrate these checks.
+- New demo `LeanPlot.Demos.InvalidDataDemo.lean` to showcase the warning banner with functions producing `NaN`/`Infinity`.
+
+### Changed
+
+- N/A
+
+### Fixed
+
+- Corrected block comment syntax in `LeanPlot/Utils.lean` to resolve parsing errors.
+- Adjusted `open` statements in `LeanPlot/Components.lean` to correctly access `jsonDataHasInvalidFloats` from `LeanPlot.Utils`.
+
+## [0.2.3] – 2025-05-08:01:04
+
+### Added
+
+- Support for axis labels in high‐level `PlotSpec` renderer: `AxisSpec.label` is now passed through to Recharts.
+- New `PlotSpec.addSeries` combinator to append additional series to an existing plot.
+
+### Changed
+
+- Corrected construction of `AxisProps` in `PlotSpec.render` so that `dataKey?` is wrapped in `some …` as required by the `Option` type.
+
+### Fixed
+
+- N/A

DocsMain.lean

@@ -0,0 +1,19 @@
+import VersoManual
+import LeanPlotManual
+
+open Verso.Genre Manual
+
+/-- Configuration for the LeanPlot manual generation. -/
+def docsConfig : Config := {
+  emitTex := false,
+  emitHtmlSingle := false,
+  emitHtmlMulti := true,
+  htmlDepth := 2,
+  sourceLink := some "https://github.com/alok/LeanPlot",
+  issueLink := some "https://github.com/alok/LeanPlot/issues"
+}
+
+/-- Entry point for `lake exe docs`.  Generates the multi-page HTML manual into
+`docs/html-multi` (overridable via `--output` CLI flag). -/
+def main : IO UInt32 :=
+  manualMain (%doc LeanPlotManual) (config := docsConfig)

Gallery.md

@@ -5,9 +5,9 @@
 A living checklist of demo/test cases we want LeanPlot to support.  Tick items off as they are implemented.
 
 ## Line charts
-- [ ] 1-variable linear  `y = x`
-- [ ] Quadratic  `y = x²`
-- [ ] Cubic  `y = x³`
+- [x] 1-variable linear  `y = x`
+- [x] Quadratic  `y = x²`
+- [x] Cubic  `y = x³`
 - [ ] Trig periodic  `y = sin(2πx)`
 - [ ] Trig overlay  `y = sin(2πx)`, `y = cos(2πx)`
 - [ ] Damped sine  `y = e^(−3x) · sin(8πx)`

Justfile

@@ -18,7 +18,10 @@ watch:
 
 # Lint (placeholder – adjust when linter chosen)
 lint:
-	lake env lean --run Std.Tactic.Lint
+	# Ensure Batteries linter modules are freshly built with current Lean version
+	lake build +Batteries.Tactic.Lint
+	# Run Batteries linter script that checks our project modules
+	lake env lean --run .lake/packages/batteries/scripts/runLinter.lean
 
 # Clean build artefacts
 clean:
@@ -42,16 +45,16 @@ overlay:
 # Update changelog timestamp
 changelog-update:
 	python - <<'PY'
-from datetime import datetime, timezone
-stamp = datetime.now(timezone.utc).strftime('%Y-%m-%d:%H:%M')
-import pathlib, re
-path = pathlib.Path('CHANGELOG.md')
-txt = path.read_text()
-import sys, re
-new = re.sub(r'\[0\.1\.0\] – [0-9-:]+', '[0.1.0] – '+stamp, txt, count=1)
-path.write_text(new)
-print('Timestamp updated ->', stamp)
-PY
+	from datetime import datetime, timezone
+	stamp = datetime.now(timezone.utc).strftime('%Y-%m-%d:%H:%M')
+	import pathlib, re
+	path = pathlib.Path('CHANGELOG.md')
+	txt = path.read_text()
+	import sys, re
+	new = re.sub(r'\[0\.1\.0\] – [0-9-:]+', '[0.1.0] – '+stamp, txt, count=1)
+	path.write_text(new)
+	print('Timestamp updated ->', stamp)
+	PY
 
 # Docs placeholder
 docs:

LeanPlot.lean

@@ -3,3 +3,10 @@
 import LeanPlot.Basic
 import LeanPlot.Demos.OverlayPlot
 import LeanPlot.Components
+import LeanPlot.Plot
+import LeanPlot.Demos.LinearDemo
+import LeanPlot.Demos.QuadraticDemo
+import LeanPlot.Demos.OverlayDemo
+import LeanPlot.Palette
+
+