English
Given e ∈ ℤ, m ∈ ℕ and v a ValidFinite e m, the next representable value above FP.f(e,m) is obtained by either increasing the mantissa, or, if at the top exponent, returning infinity, otherwise increasing the exponent and adjusting the mantissa accordingly.
Русский
Дано e ∈ ℤ, m ∈ ℕ и v ∈ ValidFinite e m, следующая представимая сверху величина FP.f(e,m) получается либо увеличением мантисы, либо, если достигнут верхний показатель экспоненты, возвращается бесконечность, иначе увеличивается экспонента и корректируется мантиса.
LaTeX
$$$\\mathrm{nextUpPos}(e,m,v) = \\begin{cases} \\text{finite}(e, m+1) & \\text{if } m' = m.\\mathrm{succ} \\\\ & \\text{allows same size} \\,; \\\\ \\text{inf} & \\text{if } e = \\mathrm{emax} \\\\ \\text{finite}(e+1, \\lfloor m'/2 \\rfloor) & \\text{otherwise} \\end{cases}$, \\\\ m' := m.\\mathrm{succ}$$$
Lean4
@[nolint docBlame]
unsafe def ofPosRatDn (n : ℕ+) (d : ℕ+) : Float × Bool :=
by
let e₁ : ℤ := n.1.size - d.1.size - prec
obtain ⟨d₁, n₁⟩ := Int.shift2 d.1 n.1 (e₁ + prec)
let e₂ := if n₁ < d₁ then e₁ - 1 else e₁
let e₃ := max e₂ emin
obtain ⟨d₂, n₂⟩ := Int.shift2 d.1 n.1 (e₃ + prec)
let r := mkRat n₂ d₂
let m := r.floor
refine (Float.finite Bool.false e₃ (Int.toNat m) ?_, r.den = 1)
exact lcProof
