English
Given positive natural numbers n and d, the function ofPosRatDn computes a finite FP.Float along with a boolean flag indicating exactness, using a sequence of shifts and exponent choices to approximate the positive rational n/d.
Русский
Для положительных натуральных чисел n и d функция ofPosRatDn вычисляет конечное FP.Float вместе с булевым флагом точности, используя последовательность сдвигов и выбор экспоненты для аппроксимации положительного дробного числа n/d.
LaTeX
$$$\\text{ofPosRatDn} : \\mathbb{N}_{+} \\times \\mathbb{N}_{+} \\to \\text{FP.Float} \\times \\{\\text{Bool}\\}$, \\\\ \\text{эквивалентно процессу выбора величины и точности через последовательность шагов}$$$
Lean4
@[nolint docBlame]
unsafe def ofRatUp : ℚ → Float
| ⟨0, _, _, _⟩ => Float.zero false
| ⟨Nat.succ n, d, h, _⟩ =>
let (f, exact) := ofPosRatDn n.succPNat ⟨d, Nat.pos_of_ne_zero h⟩
if exact then f else nextUp f
| ⟨Int.negSucc n, d, h, _⟩ => Float.neg (ofPosRatDn n.succPNat ⟨d, Nat.pos_of_ne_zero h⟩).1
