English
Given e ∈ ℤ, m ∈ ℕ and v a ValidFinite e m, the next representable value below FP.f(e,m) is obtained by stepping down or, if at the minimum, adjusting toward the lower bound, potentially reaching the minimum or finite values, otherwise decreasing the exponent and increasing the mantissa.
Русский
Дано e ∈ ℤ, m ∈ ℕ и v ∈ ValidFinite e m, следующая являющаяся представимой величина снизу выполняется аналогично: либо уменьшается мантиса, либо если достигнуто минимальное, двигаемся к нижней границе, возможно достигая минумум или конечные значения, иначе уменьшается экспонента и увеличивается мантиса.
LaTeX
$$$\\mathrm{nextDnPos}(e,m,v) = \\begin{cases} \\mathrm{nextUpPos}(-e-1, \\cdot) & \\text{при некоторых условиях} \\\\ \\text{finite}(e-1, 2m+1) & \\text{иначе} \end{cases}$$$
Lean4
@[nolint docBlame]
unsafe def nextUpPos (e m) (v : ValidFinite e m) : Float :=
let m' := m.succ
if ss : m'.size = m.size then Float.finite false e m' (by unfold ValidFinite at *; rw [ss]; exact v)
else if h : e = emax then Float.inf false else Float.finite false e.succ (Nat.div2 m') lcProof
