3.3. The #plot Command
The #plot command is defined in LeanPlot.DSL and provides convenient syntax
for plotting functions:
#plot (fun x => x^2)
#plot (fun x => Float.sin x) using 400
3.3.1. Doc Comments as Captions
You can add a doc comment before #plot to display a caption above the chart:
/-- The classic parabola y = x² -/
#plot (fun x => x^2)
This acts as a "poor man's legend" – the doc string appears as a title above the rendered chart when you hover.
Behind the scenes, #plot f expands to #html LeanPlot.API.plot f.
For expressions that already return Html (like plotMany), use #html directly:
#html plotMany #[("sin", Float.sin), ("cos", Float.cos)]