4.1. Zero-Config Functions🔗

These progressive disclosure Tier-0 functions require no configuration.

4.1.1. plot🔗

Plot a single function with automatic styling and axis labels.

plot example

#plot (fun x => x^2)

def

LeanPlot.API.plot.{u_1} {β : Type u_1} [LeanPlot.ToFloat β]
  (f : Float → β) (steps : Nat := 200)
  (domain : Option (Float × Float) := none)
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat := LeanPlot.Constants.defaultH) : ProofWidgets.Html
LeanPlot.API.plot.{u_1} {β : Type u_1}
  [LeanPlot.ToFloat β] (f : Float → β)
  (steps : Nat := 200)
  (domain : Option (Float × Float) :=
    none)
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat :=
    LeanPlot.Constants.defaultH) :
  ProofWidgets.Html

Simple line chart - Just pass your function, get beautiful plot!

Examples:

#plot plot (fun t => t^2) - Automatic "time" labels
#plot plot (fun x => Float.sin x) - Automatic "x" labels
#plot plot (fun i => i * 3) (steps := 100) - Custom sample count

This is the new recommended way to plot functions. Zero configuration needed!

4.1.2. plotMany🔗

Compare multiple functions on a single chart with automatic colors and legend.

plotMany example

#html plotMany #[("sin", fun x => Float.sin x), ("cos", fun x => Float.cos x)]

def

LeanPlot.API.plotMany.{u_1} {β : Type u_1} [LeanPlot.ToFloat β]
  (fns : Array (String × (Float → β))) (steps : Nat := 200)
  (domain : Float × Float := (0.0, 1.0))
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat := LeanPlot.Constants.defaultH) : ProofWidgets.Html
LeanPlot.API.plotMany.{u_1} {β : Type u_1}
  [LeanPlot.ToFloat β]
  (fns : Array (String × (Float → β)))
  (steps : Nat := 200)
  (domain : Float × Float := (0.0, 1.0))
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat :=
    LeanPlot.Constants.defaultH) :
  ProofWidgets.Html

Simple multi-function plot - Multiple functions, automatic everything!

Examples:

#plot plotMany #[("sin", fun x => Float.sin x), ("cos", fun x => Float.cos x)]
#plot plotMany #[("linear", fun t => t), ("quadratic", fun t => t^2)] (domain := (0.0, 2.0))

Automatic colors, legend, and labels. Perfect for comparing functions!

4.1.3. scatter🔗

Create scatter plots for visualizing discrete data points.

scatter example

#html scatter (fun x => x^2 + 0.1 * Float.sin (10 * x)) (steps := 50)

def

LeanPlot.API.scatter.{u_1} {β : Type u_1} [LeanPlot.ToFloat β]
  (f : Float → β) (steps : Nat := 200)
  (domain : Option (Float × Float) := none)
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat := LeanPlot.Constants.defaultH) : ProofWidgets.Html
LeanPlot.API.scatter.{u_1} {β : Type u_1}
  [LeanPlot.ToFloat β] (f : Float → β)
  (steps : Nat := 200)
  (domain : Option (Float × Float) :=
    none)
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat :=
    LeanPlot.Constants.defaultH) :
  ProofWidgets.Html

Simple scatter plot - Points with automatic styling!

Examples:

#plot scatter (fun x => x + Random.rand) - Show function with noise
#plot scatter (fun t => Float.sin t) (steps := 50) - Fewer points

4.1.4. bar🔗

Create bar charts for discrete or categorical data.

#html bar (fun i => i^2) (steps := 10)

def

LeanPlot.API.bar.{u_1} {β : Type u_1} [LeanPlot.ToFloat β]
  (f : Float → β) (steps : Nat := 200)
  (domain : Option (Float × Float) := none)
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat := LeanPlot.Constants.defaultH) : ProofWidgets.Html
LeanPlot.API.bar.{u_1} {β : Type u_1}
  [LeanPlot.ToFloat β] (f : Float → β)
  (steps : Nat := 200)
  (domain : Option (Float × Float) :=
    none)
  (w : Nat := LeanPlot.Constants.defaultW)
  (h : Nat :=
    LeanPlot.Constants.defaultH) :
  ProofWidgets.Html

Simple bar chart - Bars with automatic styling!

Examples:

#plot bar (fun i => i^2) (steps := 10) - Discrete function as bars
#plot bar (fun x => Float.floor x) (steps := 20) - Step function