English
For a finite FP.Float f = Float.finite s e m, let (n,d) = Int.shift2 m 1 e and r = mkRat n d. Then toRat f equals -r if s is true, otherwise r.
Русский
Для конечного FP.Float f = Float.finite s e m пусть (n,d) = Int.shift2 m 1 e и r = mkRat n d. Тогда toRat f равно -r, если s истинно, иначе r.
LaTeX
$$$\\text{toRat}(\\text{Float.finite } s\\ e\\ m) = \\begin{cases} -\\mathrm{mkRat}(n,d) & \\text{if } s, \\\\ \\mathrm{mkRat}(n,d) & \\text{otherwise} \\end{cases}, \\quad \\text{где } (n,d) = \\mathrm{Int}.\\text{shift2}(m,1,e)$$$
Lean4
@[nolint docBlame]
def toRat : ∀ f : Float, f.isFinite → ℚ
| Float.finite s e m _, _ =>
let (n, d) := Int.shift2 m 1 e
let r := mkRat n d
if s then -r else r
