Skip to content

Commit 49dcede

Browse files
committed
docs: Fix Verso code blocks and {name} roles
- Add imports to Concepts.lean for code elaboration - Mark code blocks as ```lean for hover info - Use full paths for {name} roles (LeanPlot.Components.sample) - Fix scatter example (remove undefined noise variable) - Use {name} roles for function references
1 parent da836bd commit 49dcede

2 files changed

Lines changed: 12 additions & 7 deletions

File tree

doc/Manual/API.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ tag := "api-reference"
2020
LeanPlot provides a layered API following {deftech}_progressive disclosure_:
2121

2222
1. *Tier 0 (Zero-Config)*: Functions like {name}`plot`, {name}`plotMany`, {name}`scatter`, and {name}`bar` that just work
23-
2. *Tier 1 (Components)*: Mid-level functions like {name}`sample` and `mkLineChart` for more control
23+
2. *Tier 1 (Components)*: Mid-level functions like {name}`LeanPlot.Components.sample` and `mkLineChart` for more control
2424
3. *Tier 2 (Recharts)*: Direct access to Recharts JSX components for full customization
2525

2626
# Zero-Config Functions
@@ -70,7 +70,7 @@ Create scatter plots for visualizing discrete data points.
7070
![scatter example](img/scatter_demo.svg)
7171

7272
```lean
73-
#html scatter (fun x => x^2 + noise) (steps := 50)
73+
#html scatter (fun x => x^2 + 0.1 * Float.sin (10 * x)) (steps := 50)
7474
```
7575

7676
{docstring LeanPlot.API.scatter}

doc/Manual/Concepts.lean

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,12 @@ Released under Apache 2.0 license.
44
-/
55
import VersoManual
66
import Manual.Meta
7+
import LeanPlot.API
8+
import LeanPlot.DSL
79

810
open Verso.Genre Manual
911
open Verso.Genre.Manual.InlineLean
12+
open LeanPlot.API
1013

1114
set_option pp.rawOnError true
1215

@@ -28,8 +31,8 @@ while advanced customization is still possible when needed.
2831

2932
The three tiers are:
3033

31-
1. *Tier 0 (Zero-Config)*: One-liner helpers like `plot`, `scatter`, `bar`
32-
2. *Tier 1 (Components)*: Building blocks like `sample`, `mkLineChart`
34+
1. *Tier 0 (Zero-Config)*: One-liner helpers like {name}`plot`, {name}`scatter`, {name}`bar`
35+
2. *Tier 1 (Components)*: Building blocks like {name}`LeanPlot.Components.sample`, `mkLineChart`
3336
3. *Tier 2 (Recharts)*: Direct JSX access for full control
3437

3538
Most users only need Tier 0. The other tiers exist for when you need
@@ -66,18 +69,20 @@ tag := "plot-command"
6669
The `#plot` command is defined in `LeanPlot.DSL` and provides convenient syntax
6770
for plotting functions:
6871

69-
```
72+
```lean
7073
-- Basic usage
7174
#plot (fun x => x^2)
75+
```
7276

77+
```lean
7378
-- With custom sample count
7479
#plot (fun x => Float.sin x) using 400
7580
```
7681

7782
Behind the scenes, `#plot f` expands to `#html LeanPlot.API.plot f`.
7883

79-
For expressions that already return `Html` (like `plotMany`), use `#html` directly:
84+
For expressions that already return `Html` (like {name}`plotMany`), use `#html` directly:
8085

81-
```
86+
```lean
8287
#html plotMany #[("sin", Float.sin), ("cos", Float.cos)]
8388
```

0 commit comments

Comments
 (0)