4.2. Components Layer🔗

The components layer provides more control over chart construction.

4.2.1. sample🔗

def

LeanPlot.Components.sample.{u_1} {β : Type u_1} [LeanPlot.ToFloat β]
  (f : Float → β) (steps : Nat := 200)
  (domainOpt : Option (Float × Float) := none) : Array Lean.Json
LeanPlot.Components.sample.{u_1}
  {β : Type u_1} [LeanPlot.ToFloat β]
  (f : Float → β) (steps : Nat := 200)
  (domainOpt : Option (Float × Float) :=
    none) :
  Array Lean.Json

Uniformly sample a function f : Float → β on the interval [min,max] or an auto-detected domain. β is required to have a [ToFloat β] instance so that values can be converted to a JavaScript-friendly Float for serialisation.

4.2.2. sampleMany🔗

def

LeanPlot.Components.sampleMany.{u_1} {β : Type u_1} [LeanPlot.ToFloat β]
  (fns : Array (String × (Float → β))) (steps : Nat := 200)
  (min : Float := 0) (max : Float := 1) : Array Lean.Json
LeanPlot.Components.sampleMany.{u_1}
  {β : Type u_1} [LeanPlot.ToFloat β]
  (fns : Array (String × (Float → β)))
  (steps : Nat := 200) (min : Float := 0)
  (max : Float := 1) : Array Lean.Json

Sample several functions whose outputs will be stored under the given series names. Each function must return a type with a [ToFloat] instance so that the value can be serialised.