4.3. The ToFloat Typeclass🔗

type class

LeanPlot.ToFloat.{u} (α : Type u) : Type u
LeanPlot.ToFloat.{u} (α : Type u) : Type u

Typeclass for converting a value to a Float. The conversion might be lossy (e.g. when the input is Int or Nat). The design purpose is not to provide a formal embedding – merely a convenient bridge for visualisation where Float is the lingua franca of JS charting libraries.

Instance Constructor

LeanPlot.ToFloat.mk.{u}

Methods

toFloat : α → Float

Convert a value to a Float.

This typeclass allows plotting functions that return any numeric type, not just Float. Built-in instances exist for Float, Nat, Int, and Rat.