def definition def or abbrev

`to_seconds`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 307@[simp] noncomputable def to_seconds (cal : ExternalCalibration) (t : Time) : ℝ :=

Definition body.

 308  t * cal.seconds_per_tick
 309
 310/-- Convert length (in voxels) to meters. -/

From the project-wide theorem graph. These declarations reference this one in their body.

measure_to_seconds in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use
to_seconds in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use

Lean names referenced from this declaration's body.

ExternalCalibration in IndisputableMonolith.Constants.RSNativeUnits decl_use
Time in IndisputableMonolith.Constants.RSNativeUnits decl_use
to_seconds in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use