Host-backed source math capabilities implemented by Lean's actual binary32/binary64 C math bindings. Bits cross the boundary unchanged; the source math interpreter remains responsible for NaN adjustment and the configured error perturbation. Unsupported source widths and operations stay visible at the exact host callback that requests them.
Lean's bundled Float API exposes only a subset of libc's C math functions.
These direct scalar externs use the Linux libc symbols called by pinned
std::num::{f32,f64} on the required Linux host.
Adapter for real Linux host math operations. Binary16 paths are enabled only where pinned core/std promotes to a corresponding f32 operation.
Equations
- One or more equations did not get rendered due to their size.